1. Fermat's Little Theorem
Definition1.1
Group: Fermat's Little Theorem. (10)
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.2
Associated Lean declarations
-
FermatLittleTheorem[complete]
Fermat's Little Theorem, in integer form, says that for any prime p and
integer a, one has a^p \equiv a \pmod p.
Lean code for Definition1.1●1 definition
Associated Lean declarations
-
FermatLittleTheorem[complete]
Associated Lean declarations
-
FermatLittleTheorem[complete]
-
defdefined in DifferentProofs/FermatLittleTheorem/Defs.leancomplete
def FermatLittleTheorem
FermatLittleTheorem : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.def FermatLittleTheorem
FermatLittleTheorem : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.
Definition1.2
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
-
FermatLittleTheoremNat[complete]
The natural-number form says that for any prime p and natural number a,
one has a^p \equiv a \pmod p.
Lean code for Definition1.2●1 definition
Associated Lean declarations
-
FermatLittleTheoremNat[complete]
Associated Lean declarations
-
FermatLittleTheoremNat[complete]
-
defdefined in DifferentProofs/FermatLittleTheorem/Defs.leancomplete
def FermatLittleTheoremNat
FermatLittleTheoremNat : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.def FermatLittleTheoremNat
FermatLittleTheoremNat : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.
Theorem1.3
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
Used by 2
Preview
Theorem 1.7
The natural-number statement Definition 1.2 implies the integer statement Definition 1.1.
Lean code for Theorem1.3●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Basic.leancomplete
theorem FermatLittleTheoremNat_impl_FermatLittleTheorem
FermatLittleTheoremNat_impl_FermatLittleTheorem : FermatLittleTheoremNat → FermatLittleTheorem: FermatLittleTheoremNatFermatLittleTheoremNat : Prop→ FermatLittleTheoremFermatLittleTheorem : Proptheorem FermatLittleTheoremNat_impl_FermatLittleTheorem
FermatLittleTheoremNat_impl_FermatLittleTheorem : FermatLittleTheoremNat → FermatLittleTheorem: FermatLittleTheoremNatFermatLittleTheoremNat : Prop→ FermatLittleTheoremFermatLittleTheorem : Prop
Proof for Theorem 1.3
Work in \mathbb{Z}/p\mathbb{Z}. Every element is represented by the natural
number ((a : ZMod p).val), so the natural-number congruence transfers back
through the canonical map.
First proof uses the binomial theorem.
Theorem1.4
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
-
FermatLittleTheorem_Binomial[complete]
For any prime p and integer a, one has a^p \equiv a \pmod p.
Lean code for Theorem1.4●1 theorem
Associated Lean declarations
-
FermatLittleTheorem_Binomial[complete]
Associated Lean declarations
-
FermatLittleTheorem_Binomial[complete]
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Binomial.leancomplete
theorem FermatLittleTheorem_Binomial
FermatLittleTheorem_Binomial : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Proptheorem FermatLittleTheorem_Binomial
FermatLittleTheorem_Binomial : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Prop
Proof for Theorem 1.4
In characteristic p, Freshman's dream gives
(x + 1)^p = x^p + 1. Applying this in ZMod p and inducting over natural
representatives proves the congruence.
Second proof uses Lagrange's theorem on groups, applied to the multiplicative group of units in \mathbb{Z}/p\mathbb{Z}.
Theorem1.5
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
-
FermatLittleTheorem_Lagrange[complete]
For any prime p and integer a, one has a^p \equiv a \pmod p.
Lean code for Theorem1.5●1 theorem
Associated Lean declarations
-
FermatLittleTheorem_Lagrange[complete]
Associated Lean declarations
-
FermatLittleTheorem_Lagrange[complete]
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Lagrange.leancomplete
theorem FermatLittleTheorem_Lagrange
FermatLittleTheorem_Lagrange : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Proptheorem FermatLittleTheorem_Lagrange
FermatLittleTheorem_Lagrange : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Prop
Proof for Theorem 1.5
If a is zero modulo p, the claim is immediate. Otherwise a is a unit in
\mathbb{Z}/p\mathbb{Z}; by Lagrange's theorem its order divides
p - 1, so a^{p-1} = 1, and multiplying by a gives the result.
Third proof is by Alkauskas. It is based on a formal product expansion of a certain rational function, which is used to derive the natural-number form of Fermat's Little Theorem.
Lemma1.6
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
Let g \in \mathbb{Z}[[x]] be an integer power series of the form
g(x) = 1 - x - d x^2 + \sum_{k \ge 3} b_k x^k. For every N, there is a
sequence of integers (a_n)_{n \ge 1} with a_1 = 1 such that g agrees
with \prod_{n=1}^{N}(1 - a_n x^n) in all coefficients of degree at most
N.
Lean code for Lemma1.6●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Alkauskas.leancomplete
theorem FermatLittleTheorem.Alkauskas.exists_intExpansion
FermatLittleTheorem.Alkauskas.exists_intExpansion {g : PowerSeries ℤ} (hg0 : PowerSeries.constantCoeff g = 1) (hg1 : (PowerSeries.coeff 1) g = -1) (N : ℕ) : ∃ a, a 1 = 1 ∧ ∀ k ≤ N, (PowerSeries.coeff k) g = (PowerSeries.coeff k) (∏ n ∈ Finset.Icc 1 N, (1 - PowerSeries.C (a n) * PowerSeries.X ^ n)){gPowerSeries ℤ: PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).} (hg0PowerSeries.constantCoeff g = 1: PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.gPowerSeries ℤ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.1) (hg1(PowerSeries.coeff 1) g = -1: (PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.1) gPowerSeries ℤ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.-1) (Nℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ∃ aℕ → ℤ, aℕ → ℤ1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.1 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.∀ kℕ≤ Nℕ, (PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.kℕ) gPowerSeries ℤ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.(PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.kℕ) (∏ nℕ∈ Finset.IccFinset.Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset αThe finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a finset.1 Nℕ, (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).PowerSeries.CPowerSeries.C.{u_1} {R : Type u_1} [Semiring R] : R →+* PowerSeries RThe constant formal power series.(aℕ → ℤnℕ) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring.^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `^` in identifiers is `pow`.nℕ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).)theorem FermatLittleTheorem.Alkauskas.exists_intExpansion
FermatLittleTheorem.Alkauskas.exists_intExpansion {g : PowerSeries ℤ} (hg0 : PowerSeries.constantCoeff g = 1) (hg1 : (PowerSeries.coeff 1) g = -1) (N : ℕ) : ∃ a, a 1 = 1 ∧ ∀ k ≤ N, (PowerSeries.coeff k) g = (PowerSeries.coeff k) (∏ n ∈ Finset.Icc 1 N, (1 - PowerSeries.C (a n) * PowerSeries.X ^ n)){gPowerSeries ℤ: PowerSeriesPowerSeries.{u_1} (R : Type u_1) : Type u_1Formal power series over a coefficient type `R`ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).} (hg0PowerSeries.constantCoeff g = 1: PowerSeries.constantCoeffPowerSeries.constantCoeff.{u_1} {R : Type u_1} [Semiring R] : PowerSeries R →+* RThe constant coefficient of a formal power series.gPowerSeries ℤ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.1) (hg1(PowerSeries.coeff 1) g = -1: (PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.1) gPowerSeries ℤ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.-1) (Nℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ∃ aℕ → ℤ, aℕ → ℤ1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.1 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.∀ kℕ≤ Nℕ, (PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.kℕ) gPowerSeries ℤ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.(PowerSeries.coeffPowerSeries.coeff.{u_1} {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] RThe `n`th coefficient of a formal power series.kℕ) (∏ nℕ∈ Finset.IccFinset.Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset αThe finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a finset.1 Nℕ, (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).PowerSeries.CPowerSeries.C.{u_1} {R : Type u_1} [Semiring R] : R →+* PowerSeries RThe constant formal power series.(aℕ → ℤnℕ) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.PowerSeries.XPowerSeries.X.{u_1} {R : Type u_1} [Semiring R] : PowerSeries RThe variable of the formal power series ring.^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `^` in identifiers is `pow`.nℕ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).)
Proof for Lemma 1.6
Choose the factors inductively. Multiplying by
1 - a_{N+1}x^{N+1} leaves all lower coefficients fixed, and the integer
a_{N+1} can be chosen to match the coefficient of x^{N+1}.
Theorem1.7
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
For any prime p and integer a, one has a^p \equiv a \pmod p.
Lean code for Theorem1.7●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Alkauskas.leancomplete
theorem FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Proptheorem FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Prop
Proof for Theorem 1.7
Apply the integer formal product expansion Lemma 1.6
to \frac{1-(d+1)x}{1-dx}. Comparing the coefficient of x^p in the negated
logarithmic derivative gives p \mid (d+1)^p - d^p - 1. Telescoping these
congruences over d proves the natural-number form, then the reduction
Theorem 1.3 gives the integer form.
Fourth proof is by a dynamical argument, using the map T_n : [0,1] \to [0,1]
defined by T_n(x) = \{nx\} for 0 \le x < 1 and T_n(1) = 1, and considering the fixed points of T_{a^p} that are not fixed by T_a.
Definition1.8
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Lemma 1.9
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
-
T[complete]
Used by 2
Preview
Lemma 1.9
For a natural number n, define T_n : [0,1] \to [0,1] by
T_n(x) = \{nx\} for 0 \le x < 1 and T_n(1) = 1.
Lean code for Definition1.8●1 definition
Associated Lean declarations
-
T[complete]
Associated Lean declarations
-
T[complete]
-
defdefined in DifferentProofs/FermatLittleTheorem/Dynamical.leancomplete
def T
T (n : ℕ) (x : ↑unitInterval) : ↑unitInterval(nℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) (x↑unitInterval: ↑unitIntervalunitInterval : Set ℝThe unit interval `[0,1]` in ℝ.) : ↑unitIntervalunitInterval : Set ℝThe unit interval `[0,1]` in ℝ.def T
T (n : ℕ) (x : ↑unitInterval) : ↑unitInterval(nℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) (x↑unitInterval: ↑unitIntervalunitInterval : Set ℝThe unit interval `[0,1]` in ℝ.) : ↑unitIntervalunitInterval : Set ℝThe unit interval `[0,1]` in ℝ.
Lemma1.9
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.10
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
-
T_comp_eq_mul[complete]
For natural numbers m and n, the maps satisfy
T_m \circ T_n = T_{mn}. This is a consequence of Definition 1.8.
Lean code for Lemma1.9●1 theorem
Associated Lean declarations
-
T_comp_eq_mul[complete]
Associated Lean declarations
-
T_comp_eq_mul[complete]
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Dynamical.leancomplete
theorem T_comp_eq_mul
T_comp_eq_mul (m n : ℕ) : T m ∘ T n = T (m * n)(mℕnℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : TT (n : ℕ) (x : ↑unitInterval) : ↑unitIntervalmℕ∘Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δFunction composition, usually written with the infix operator `∘`. A new function is created from two existing functions, where one function's output is used as input to the other. Examples: * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]` * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]` Conventions for notations in identifiers: * The recommended spelling of `∘` in identifiers is `comp`.TT (n : ℕ) (x : ↑unitInterval) : ↑unitIntervalnℕ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.TT (n : ℕ) (x : ↑unitInterval) : ↑unitInterval(HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.mℕ*HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.nℕ)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.theorem T_comp_eq_mul
T_comp_eq_mul (m n : ℕ) : T m ∘ T n = T (m * n)(mℕnℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : TT (n : ℕ) (x : ↑unitInterval) : ↑unitIntervalmℕ∘Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δFunction composition, usually written with the infix operator `∘`. A new function is created from two existing functions, where one function's output is used as input to the other. Examples: * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]` * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]` Conventions for notations in identifiers: * The recommended spelling of `∘` in identifiers is `comp`.TT (n : ℕ) (x : ↑unitInterval) : ↑unitIntervalnℕ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.TT (n : ℕ) (x : ↑unitInterval) : ↑unitInterval(HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.mℕ*HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.nℕ)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.
Proof for Lemma 1.9
Away from 1, write fractional parts as subtraction of floors:
\{m\{nx\}\} = \{mnx\} because the difference is an integer.
The endpoint 1 is fixed by definition.
Lemma1.10
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Theorem 1.11
Preview
Definition 1.1
Associated Lean declarations
-
T_num_fp_eq[complete]
For any n \ge 2, the map T_n has exactly n fixed points.
This counts the fixed points of Definition 1.8.
Lean code for Lemma1.10●1 theorem
Associated Lean declarations
-
T_num_fp_eq[complete]
Associated Lean declarations
-
T_num_fp_eq[complete]
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Dynamical.leancomplete
theorem T_num_fp_eq
T_num_fp_eq (n : ℕ) (hn : 2 ≤ n) : Nat.card ↑{x | T n x = x} = n(nℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) (hn2 ≤ n: 2 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` Conventions for notations in identifiers: * The recommended spelling of `≤` in identifiers is `le`.nℕ) : Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number. If `α` is infinite, `Nat.card α = 0`.↑{setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}`x↑unitInterval|setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}`TT (n : ℕ) (x : ↑unitInterval) : ↑unitIntervalnℕx↑unitInterval=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.x↑unitInterval}setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}`=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.nℕtheorem T_num_fp_eq
T_num_fp_eq (n : ℕ) (hn : 2 ≤ n) : Nat.card ↑{x | T n x = x} = n(nℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) (hn2 ≤ n: 2 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` Conventions for notations in identifiers: * The recommended spelling of `≤` in identifiers is `le`.nℕ) : Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number. If `α` is infinite, `Nat.card α = 0`.↑{setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}`x↑unitInterval|setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}`TT (n : ℕ) (x : ↑unitInterval) : ↑unitIntervalnℕx↑unitInterval=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.x↑unitInterval}setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}`=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.nℕ
Proof for Lemma 1.10
For x < 1, the equation T_n(x)=x is equivalent to
(n-1)x \in \mathbb{Z}, giving the points j/(n-1) for
0 \le j \le n-2. Together with the endpoint 1, these are exactly
n fixed points.
Theorem1.11
Group: Fermat's Little Theorem. (10)
- Definition 1.1
- Definition 1.2
- Theorem 1.3
- Theorem 1.4
- Theorem 1.5
- Lemma 1.6
- Theorem 1.7
- Definition 1.8
- Lemma 1.9
- Lemma 1.10
Preview
Definition 1.1
Associated Lean declarations
-
FermatLittleTheorem_Dynamical[complete]
For any prime p and integer a, one has a^p \equiv a \pmod p.
The proof uses Lemma 1.9, Lemma 1.10, and
the reduction Theorem 1.3.
Lean code for Theorem1.11●1 theorem
Associated Lean declarations
-
FermatLittleTheorem_Dynamical[complete]
Associated Lean declarations
-
FermatLittleTheorem_Dynamical[complete]
-
theoremdefined in DifferentProofs/FermatLittleTheorem/Dynamical.leancomplete
theorem FermatLittleTheorem_Dynamical
FermatLittleTheorem_Dynamical : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Proptheorem FermatLittleTheorem_Dynamical
FermatLittleTheorem_Dynamical : FermatLittleTheorem: FermatLittleTheoremFermatLittleTheorem : Prop
Proof for Theorem 1.11
By Theorem 1.3, it suffices to prove the natural-number form.
It suffices to prove the natural-number form. For a \ge 2, consider the
fixed points of T_{a^p} that are not fixed by T_a. Their cardinality is
a^p-a, and the action of T_a partitions this set into orbits of size
p, so p divides a^p-a.