FiniteField.card
theorem FiniteField.card :
∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (p : ℕ) [inst : CharP K p],
∃ n, p.Prime ∧ Fintype.card K = p ^ ↑n
The theorem `FiniteField.card` states that for any type `K` that has a field structure and is finite (i.e., has a finite number of elements), and for any natural number `p` that has the property of being the characteristic of `K`, there exists some natural number `n` such that `p` is prime and the number of elements in `K` (denoted `Fintype.card K`) equals `p` to the power `n`. In other words, the cardinality of a finite field is always a prime number raised to some power.
More concisely: The cardinality of a finite field is a prime number raised to some power.
|
FiniteField.isSquare_iff
theorem FiniteField.isSquare_iff :
∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F],
ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → (IsSquare a ↔ a ^ (Fintype.card F / 2) = 1)
The theorem `FiniteField.isSquare_iff` states that for any finite field `F` with characteristic not equal to 2 and any non-zero element `a` of `F`, `a` is a square if and only if `a` raised to the power of half the number of elements in `F` equals 1. In other words, an element in a finite field is a square precisely when its square root, raised to the cardinality of the field divided by two, equals one.
More concisely: In a finite field with characteristic not equal to 2, an element is a square if and only if its n-th power equals 1, where n is the number of elements in the field.
|
ZMod.pow_card_sub_one_eq_one
theorem ZMod.pow_card_sub_one_eq_one : ∀ {p : ℕ} [inst : Fact p.Prime] {a : ZMod p}, a ≠ 0 → a ^ (p - 1) = 1
**Fermat's Little Theorem**: This theorem asserts that for every non-zero integer `a` modulo a prime number `p` (represented as `a : ZMod p` in Lean), the integer `a` raised to the power of `p - 1` is congruent to 1. In mathematical notation, this is expressed as `a^(p - 1) ≡ 1 (mod p)`. The theorem is applicable only for prime numbers `p` and non-zero `a`.
More concisely: For any prime number `p` and non-zero integer `a`, `a^(p-1)` is congruent to 1 modulo `p`.
|
FiniteField.X_pow_card_sub_X_natDegree_eq
theorem FiniteField.X_pow_card_sub_X_natDegree_eq :
∀ (K' : Type u_3) [inst : Field K'] {p : ℕ}, 1 < p → (Polynomial.X ^ p - Polynomial.X).natDegree = p
This theorem states that for any given type `K'` that forms a field and any natural number `p` greater than 1, the natural degree (which is a non-negative integer representation of the degree) of the polynomial obtained by raising the polynomial variable `X` to the power `p` and then subtracting `X` itself is equal to `p`. This essentially states that the highest power of `X` in the polynomial `X^p - X` is `p`.
More concisely: For any field `K` and natural number `p > 1`, the degree of the polynomial `X^p - X` over `K` is equal to `p`.
|
FiniteField.pow_card
theorem FiniteField.pow_card :
∀ {K : Type u_1} [inst : GroupWithZero K] [inst_1 : Fintype K] (a : K), a ^ Fintype.card K = a
The theorem `FiniteField.pow_card` states that for any type `K` which has structures of a group with zero and a finite type, any element `a` of `K` raised to the power of the cardinality of `K` (that is, the number of distinct elements in `K`) equals to the element `a` itself. In mathematical terms, for any `a` in `K` we have the equation $a^{card(K)} = a$, where `card(K)` denotes the number of elements in `K`.
More concisely: For any element `a` in a finite group `K`, we have `a^(|K|) = a`, where `|K|` denotes the number of elements in `K`.
|
FiniteField.pow_dichotomy
theorem FiniteField.pow_dichotomy :
∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F],
ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
The theorem `FiniteField.pow_dichotomy` states that for any finite field `F` with an odd characteristic, and for any non-zero element `a` of `F`, the value of `a` raised to the power of half the number of elements in `F` is either 1 or -1. This means that in such a finite field with an odd characteristic, taking the square root of a non-zero element results in either 1 or -1.
More concisely: For any finite field `F` with odd characteristic and any non-zero element `a` in `F`, `a^(card F / 2)` equals `1` or `-1`.
|
FiniteField.sum_pow_lt_card_sub_one
theorem FiniteField.sum_pow_lt_card_sub_one :
∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K],
∀ i < Fintype.card K - 1, (Finset.univ.sum fun x => x ^ i) = 0
The theorem `FiniteField.sum_pow_lt_card_sub_one` states that for any finite field `K` with cardinality `q` (`Fintype.card K`), the sum of `x ^ i` for every element `x` in the field is equal to `0` if `i` is less than `q - 1`. In other words, the sum of each element of the finite field raised to a power less than one less than the field's cardinality is zero.
More concisely: For any finite field K of cardinality q, the sum of x^i for all i in K with i < q is zero.
|
ZMod.expand_card
theorem ZMod.expand_card :
∀ {p : ℕ} [inst : Fact p.Prime] (f : Polynomial (ZMod p)), (Polynomial.expand (ZMod p) p) f = f ^ p
This theorem states that for every prime number `p` and any polynomial `f` with coefficients in the integers modulo `p`, when we expand the polynomial `f` by a factor of `p` (i.e., transform each term `aₙ xⁿ` to `aₙ xⁿᵖ`), the result is equivalent to raising the polynomial `f` to the power of `p`. In mathematical terms, for every prime `p` and a polynomial `f` in ℤ/pℤ, (f(x))^p is the same as f(x^p).
More concisely: For every prime number `p`, expanding a polynomial `f` in ℤ/pℤ by a factor of `p` is equivalent to raising `f` to the power of `p`.
|
FiniteField.card_image_polynomial_eval
theorem FiniteField.card_image_polynomial_eval :
∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R] [inst_3 : Fintype R]
{p : Polynomial R},
0 < p.degree → Fintype.card R ≤ p.natDegree * (Finset.image (fun x => Polynomial.eval x p) Finset.univ).card
This theorem states that in a finite commutative ring `R` that is also a domain, for any polynomial `p` with a positive degree, the cardinality of the ring `R` is less than or equal to the product of the degree of the polynomial and the cardinality of the set of all values obtained by evaluating the polynomial at each element of the ring. Essentially, it's limiting the size of the field based on the number of distinct values a polynomial can take within that field.
More concisely: In a finite commutative domain `R`, the number of elements in `R` is bounded above by the degree of any non-constant polynomial over `R` times the number of elements in `R`.
|
Nat.ModEq.pow_totient
theorem Nat.ModEq.pow_totient : ∀ {x n : ℕ}, x.Coprime n → n.ModEq (x ^ n.totient) 1
This theorem is known as the Fermat-Euler totient theorem. For any natural numbers `x` and `n`, if `x` and `n` are coprime (i.e., their greatest common divisor is 1), then the remainder of `x` raised to the power of the totient of `n` when divided by `n` is `1`. Note that `ZMod.pow_totient` is another statement of the same theorem.
More concisely: If `n` is a natural number and `gcd(x, n) = 1`, then `x^φ(n) ≡ 1 (mod n)`, where `φ(n)` denotes Euler's totient function.
|
FiniteField.sum_subgroup_units
theorem FiniteField.sum_subgroup_units :
∀ {K : Type u_1} [inst : Ring K] [inst_1 : NoZeroDivisors K] {G : Subgroup Kˣ} [inst_2 : Fintype ↥G]
[inst_3 : Decidable (G = ⊥)], (Finset.univ.sum fun x => ↑↑x) = if G = ⊥ then 1 else 0
The given theorem, `FiniteField.sum_subgroup_units`, states that for any field `K` with a Ring structure without any zero divisors and a subgroup `G` of the multiplicative group of `K`, if the subgroup `G` is finite and we can decide whether `G` is the trivial group or not, the sum of all elements in this subgroup (treated as elements of `K`) is `1` if the subgroup is trivial (i.e., it only contains the unit element `1`), and `0` otherwise. Here, `Finset.univ.sum` is used to represent the sum of all elements in the finite set.
More concisely: For a finite subgroup \(G\) of the multiplicative group of a field \(K\) without zero divisors, if \(G\) is nontrivial then the sum of its elements in \(K\) is \(0\), otherwise it is \(1\).
|
Nat.sq_add_sq_modEq
theorem Nat.sq_add_sq_modEq :
∀ (p : ℕ) [inst : Fact p.Prime] (x : ℕ), ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ p.ModEq (a ^ 2 + b ^ 2) x
This theorem states that for any prime natural number `p` and any natural number `x`, there exist natural numbers `a` and `b` such that both `a` and `b` are less than or equal to `p / 2`, and the sum of the squares of `a` and `b` is congruent to `x` modulo `p`. This is a specific version of the `ZMod.sq_add_sq` theorem, which also provides estimates for the values of `a` and `b`.
More concisely: For any prime number `p` and natural number `x`, there exist integers `a` and `b` with `|a|, |b| <= p / 2` such that `a^2 + b^2 congruent x modulo p`.
|
FiniteField.sum_pow_units
theorem FiniteField.sum_pow_units :
∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] [inst_2 : DecidableEq K] (i : ℕ),
(Finset.univ.sum fun x => ↑x ^ i) = if Fintype.card K - 1 ∣ i then -1 else 0
The theorem `FiniteField.sum_pow_units` states that for any field 'K' that is finite and has decidable equality, for any natural number 'i', the sum of 'i' powers of each unit 'x' in the field is equal to zero, unless '(q - 1)' divides 'i', where 'q' is the number of elements in the field 'K'. In the case when '(q - 1)' divides 'i', the sum equals '-1'.
More concisely: For any finite field 'K' with decidable equality and unit 'x', the sum of 'i' powers of 'x' equals 0 if 'i' is not a multiple of the field size 'q', and equals -1 if 'i' is a multiple of 'q'.
|
FiniteField.unit_isSquare_iff
theorem FiniteField.unit_isSquare_iff :
∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F],
ringChar F ≠ 2 → ∀ (a : Fˣ), IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
This theorem states that for any finite field `F` with an odd characteristic, a unit `a` in `F` is a square if and only if raising `a` to the power of half the number of elements in `F` gives 1. Here, a unit `a` is a square if there exists some `r` in the field such that `a` equals `r` multiplied by `r`. The characteristic of a field is the smallest positive integer `n` such that `n` times the multiplicative identity element equals the additive identity element; in this case, the characteristic is not 2, implying it's an odd characteristic field.
More concisely: For a finite field `F` with odd characteristic, a unit `a` is a square if and only if `a^(#F/2) = 1`.
|
ZMod.units_pow_card_sub_one_eq_one
theorem ZMod.units_pow_card_sub_one_eq_one : ∀ (p : ℕ) [inst : Fact p.Prime] (a : (ZMod p)ˣ), a ^ (p - 1) = 1 := by
sorry
**Fermat's Little Theorem**: Given a prime number `p` and a unit `a` of the integers modulo `p`, the theorem asserts that `a` raised to the power of `p - 1` equals one. In other words, in the modular arithmetic with modulus equal to a prime number `p`, if you take any unit `a`, and raise it to the power of `p - 1`, the result will always be one.
More concisely: For a prime number `p` and a unit `a` modulo `p`, `a^(p-1)` equals 1.
|
FiniteField.isSquare_of_char_two
theorem FiniteField.isSquare_of_char_two :
∀ {F : Type u_3} [inst : Field F] [inst_1 : Finite F], ringChar F = 2 → ∀ (a : F), IsSquare a
This theorem states that in a finite field `F` with characteristic `2`, every element `a` of `F` is a square. In other words, for any element `a` in such a field, there exists an element `r` in the same field such that `a = r * r`. The characteristic of a field is the smallest positive integer `n` such that `n * 1 = 0` in the field, and a field is said to be of characteristic `2` if `2 * 1 = 0` in the field.
More concisely: In a finite field of characteristic 2, every non-zero element is a square.
|
FiniteField.sum_subgroup_units_eq_zero
theorem FiniteField.sum_subgroup_units_eq_zero :
∀ {K : Type u_1} [inst : Ring K] [inst_1 : NoZeroDivisors K] {G : Subgroup Kˣ} [inst_2 : Fintype ↥G],
G ≠ ⊥ → (Finset.univ.sum fun x => ↑↑x) = 0
This theorem states that for any field `K` with a ring structure and no zero divisors, and any nontrivial subgroup `G` of the multiplicative group of nonzero elements of `K`, if the subgroup `G` is finite, then the sum of all elements in this subgroup is zero. The `Finset.univ.sum` function is used to denote the sum of all elements in the group, and the function `(fun x => ↑↑x)` is used to denote the embedding of the elements of the subgroup into the field. The condition `G ≠ ⊥` is used to ensure that the subgroup is not the trivial group containing only the identity element.
More concisely: For any field `K` without zero divisors and finite, nontrivial subgroup `G` of its multiplicative group, the sum of the embedding of all elements in `G` is zero.
|
ZMod.pow_card
theorem ZMod.pow_card : ∀ {p : ℕ} [inst : Fact p.Prime] (x : ZMod p), x ^ p = x
This theorem is a variation on Fermat's Little Theorem, specifically for the integers modulo a prime number `p`. It states that for any integer `x` in the set of integers modulo `p` (where `p` is a prime number), raising `x` to the power `p` will yield `x` itself. In traditional mathematical notation, this would be stated as \(x^p \equiv x \; (mod \; p)\) for any integer `x` and prime `p`.
More concisely: For any prime number `p`, the power `x^p` equals `x` in the integers modulo `p`. (Or in mathematical notation: `x^p ≡ x (mod p)` for any integer `x` and prime `p`. )
|
FiniteField.pow_card_sub_one_eq_one
theorem FiniteField.pow_card_sub_one_eq_one :
∀ {K : Type u_1} [inst : GroupWithZero K] [inst_1 : Fintype K] (a : K), a ≠ 0 → a ^ (Fintype.card K - 1) = 1 := by
sorry
This theorem states that for any type `K` that has the structure of a group with zero along with being a finite type (indicating it has a finite number of elements), and any non-zero element `a` of type `K`, raising `a` to the power of (the number of elements in `K` minus one) will result in `1`. In mathematical terms, if `K` is a finite group and `a` is any non-zero element of `K`, then `a` to the power of (`|K|-1`) equals to `1`.
More concisely: In a finite group K, any non-zero element raised to the power of (the number of elements in K minus one) equals the identity element 1.
|
ZMod.pow_totient
theorem ZMod.pow_totient : ∀ {n : ℕ} (x : (ZMod n)ˣ), x ^ n.totient = 1
The Fermat-Euler totient theorem, represented here as `ZMod.pow_totient`, states that for any non-negative integer `n` and any unit `x` in the integers modulo `n`, the `n`-th power of `x` is equal to 1. In other words, if `x` is a unit in the ring of integers modulo `n`, then x raised to the power of the Euler's totient function of `n` (`n.totient`) is equal to 1. The `Nat.ModEq.pow_totient` theorem is an alternate statement of the same mathematical principle.
More concisely: If `n` is a positive integer and `x` is a unit in the ring of integers modulo `n`, then `x^(n.totient) = 1`.
|
Nat.sq_add_sq_zmodEq
theorem Nat.sq_add_sq_zmodEq :
∀ (p : ℕ) [inst : Fact p.Prime] (x : ℤ), ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ (↑p).ModEq (↑a ^ 2 + ↑b ^ 2) x
The theorem `Nat.sq_add_sq_zmodEq` states that for any prime natural number `p` and any integer `x`, there exist natural numbers `a` and `b` such that `a` and `b` are both less than or equal to `p / 2` and the sum of their squares is congruent to `x` modulo `p`. This theorem is a version of the `ZMod.sq_add_sq` theorem with additional constraints on the values of `a` and `b`. In mathematical terms, this means for a prime $p$ and an integer $x$, there exist natural numbers $a$ and $b$ satisfying $a \leq \frac{p}{2}$, $b \leq \frac{p}{2}$, and $a^2 + b^2 \equiv x \mod p$.
More concisely: For any prime number `p` and integer `x`, there exist natural numbers `a` and `b` with `a, b ≤ p / 2` such that `a² +b² ≡ x (mod p)`.
|
Int.ModEq.pow_card_sub_one_eq_one
theorem Int.ModEq.pow_card_sub_one_eq_one :
∀ {p : ℕ}, p.Prime → ∀ {n : ℤ}, IsCoprime n ↑p → (↑p).ModEq (n ^ (p - 1)) 1
The theorem is a statement of Fermat's Little Theorem. This theorem states that for every integer `n` that is coprime to a prime number `p`, `n` raised to the power of `p - 1` is congruent to 1 modulo `p`. In other words, if `n` and `p` share no common factors apart from 1, then the remainder of `n^(p - 1)` divided by `p` is 1. This is a fundamental theorem in number theory and plays a crucial role in cryptographical algorithms like RSA.
More concisely: For every prime number `p` and integer `n` coprime to `p`, `n^(p-1)` congruent 1 modulo `p`.
|
FiniteField.exists_nonsquare
theorem FiniteField.exists_nonsquare :
∀ {F : Type u_3} [inst : Field F] [inst_1 : Finite F], ringChar F ≠ 2 → ∃ a, ¬IsSquare a
This theorem states that in a finite field where the characteristic of the field is not 2 (i.e., the field has an odd characteristic), there exists at least one element that is not a square. Here, an element is said to be a square if it can be expressed as the product of some other element with itself. Therefore, for a field with odd characteristic, not all elements can be expressed in this manner.
More concisely: In a finite field of odd characteristic, there exists a non-square element.
|
FiniteField.exists_root_sum_quadratic
theorem FiniteField.exists_root_sum_quadratic :
∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Fintype R] {f g : Polynomial R},
f.degree = 2 → g.degree = 2 → Fintype.card R % 2 = 1 → ∃ a b, Polynomial.eval a f + Polynomial.eval b g = 0
This theorem states that given any commutative ring `R` that is also a domain and a finite type, and given any two quadratic polynomials `f` and `g` over `R`, if the number of elements in `R` is odd (`Fintype.card R % 2 = 1`), then there exist elements `a` and `b` in `R` such that the evaluation of `f` at `a` plus the evaluation of `g` at `b` equals zero (`Polynomial.eval a f + Polynomial.eval b g = 0`).
More concisely: Given a finite commutative domain ring `R`, if the number of its elements is odd, then there exist elements `a, b ∈ R` such that `Polynomial.eval a f + Polynomial.eval b g = 0` for any quadratic polynomials `f` and `g` over `R`.
|
FiniteField.odd_card_of_char_ne_two
theorem FiniteField.odd_card_of_char_ne_two :
∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F], ringChar F ≠ 2 → Fintype.card F % 2 = 1
This theorem states that for any finite field 'F', if the unique characteristic of the field (denoted by 'ringChar F') is not equal to 2, then the number of elements in the field (denoted by 'Fintype.card F') is odd. More formally, the cardinality of the field 'F' modulo 2 equals 1.
More concisely: For any finite field 'F' with characteristic different from 2, the number of elements in 'F' is odd.
|
FiniteField.even_card_iff_char_two
theorem FiniteField.even_card_iff_char_two :
∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F], ringChar F = 2 ↔ Fintype.card F % 2 = 0
This theorem states that for any finite field `F`, the field has an even number of elements if and only if its characteristic is `2`. Here, the term "characteristic" refers to the smallest number of times you have to add the multiplicative identity (1) to itself to get the additive identity (0). Therefore, the theorem is saying that the only time a finite field can have an even number of elements is when the additive identity is reached after two additions of the multiplicative identity. Conversely, if the characteristic is `2`, then the field must have an even number of elements.
More concisely: A finite field has an even number of elements if and only if its characteristic is 2.
|