Polynomial.cyclotomic'_zero
theorem Polynomial.cyclotomic'_zero :
∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.cyclotomic' 0 R = 1
This theorem states that the zeroth modified cyclotomic polynomial, with coefficients in any commutative ring `R` that is also an integral domain, is `1`. The modified cyclotomic polynomial is normally calculated as the product of polynomials `(Polynomial.X - Polynomial.C μ)` for each `μ` being a primitive `n`-th root of unity in `R`, but in this special case where `n` is zero, the result is simply `1`.
More concisely: The zeroth modified cyclotomic polynomial, as a product of `(X - μ)` for all primitive roots of unity `μ` in any commutative integral domain `R`, equals the constant polynomial `1`.
|
Polynomial.degree_cyclotomic
theorem Polynomial.degree_cyclotomic :
∀ (n : ℕ) (R : Type u_1) [inst : Ring R] [inst_1 : Nontrivial R], (Polynomial.cyclotomic n R).degree = ↑n.totient
This theorem states that for any natural number `n` and any ring `R` that is nontrivial, the degree of the `n`-th cyclotomic polynomial with coefficients in `R` is equal to the totient of `n`. The totient of a number is a function that counts the positive integers up to a given integer `n` that are relatively prime to `n`.
More concisely: The degree of the `n`-th cyclotomic polynomial over a nontrivial ring equals the totient of `n`.
|
Polynomial.cyclotomic.monic
theorem Polynomial.cyclotomic.monic : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R], (Polynomial.cyclotomic n R).Monic := by
sorry
The theorem `Polynomial.cyclotomic.monic` states that for any natural number `n` and any type `R` that forms a ring, the `n`-th cyclotomic polynomial with coefficients in `R` is a monic polynomial. A monic polynomial is defined to be one whose leading coefficient is 1.
More concisely: The `n`-th cyclotomic polynomial with coefficients in any ring `R` is a monic polynomial.
|
Polynomial.X_pow_sub_one_splits
theorem Polynomial.X_pow_sub_one_splits :
∀ {K : Type u_1} [inst : Field K] {ζ : K} {n : ℕ},
IsPrimitiveRoot ζ n → Polynomial.Splits (RingHom.id K) (Polynomial.X ^ n - Polynomial.C 1)
The theorem `Polynomial.X_pow_sub_one_splits` states that for any field `K` and any element `ζ` of `K` that is a primitive `n`-th root of unity (as specified by `IsPrimitiveRoot ζ n`), the polynomial `X^n - 1` splits over `K`. In other words, if there is a primitive `n`-th root of unity in the field `K`, then the polynomial `X^n - 1` can be factored into linear factors in `K`. The function `RingHom.id K` is the identity function on the field `K`, meaning that the coefficients of the polynomial remain in `K`. The term `Polynomial.Splits` means that the given polynomial either is the zero polynomial, or all its irreducible factors have degree 1.
More concisely: If `K` is a field with a primitive `n`-th root of unity `ζ`, then the polynomial `X^n - 1` splits over `K` into linear factors with coefficients in `K`.
|
Polynomial.map_cyclotomic
theorem Polynomial.map_cyclotomic :
∀ (n : ℕ) {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
Polynomial.map f (Polynomial.cyclotomic n R) = Polynomial.cyclotomic n S
This theorem states that the definition of the `n`-th cyclotomic polynomial over a ring `R`, denoted as `Polynomial.cyclotomic n R`, is compatible with any ring homomorphism. Specifically, if we have a ring homomorphism `f` from `R` to another ring `S`, then mapping the `n`-th cyclotomic polynomial over `R` using `f` (i.e., `Polynomial.map f (Polynomial.cyclotomic n R)`) is the same as directly computing the `n`-th cyclotomic polynomial over `S` (i.e., `Polynomial.cyclotomic n S`).
More concisely: The `n`-th cyclotomic polynomial over a ring `R` is mapped to the `n`-th cyclotomic polynomial over another ring `S` under any ring homomorphism `f` from `R` to `S`, i.e., `Polynomial.map f (Polynomial.cyclotomic n R) = Polynomial.cyclotomic n S`.
|
Polynomial.cyclotomic.isPrimitive
theorem Polynomial.cyclotomic.isPrimitive :
∀ (n : ℕ) (R : Type u_1) [inst : CommRing R], (Polynomial.cyclotomic n R).IsPrimitive
The theorem `Polynomial.cyclotomic.isPrimitive` states that for any natural number `n` and any type `R` that forms a commutative ring, the `n`-th cyclotomic polynomial with coefficients in `R` is a primitive polynomial. In mathematical terms, a primitive polynomial is a polynomial whose coefficients are integers and whose greatest common divisor is 1.
More concisely: For any natural number `n` and commutative ring `R`, the `n`-th cyclotomic polynomial over `R` has gcd of its coefficients equal to 1.
|
Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots
theorem Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots :
∀ {K : Type u_1} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
IsPrimitiveRoot ζ n →
Polynomial.cyclotomic n K = (primitiveRoots n K).prod fun μ => Polynomial.X - Polynomial.C μ
The theorem `Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots` states that, for any commutative ring `K` which is also an integral domain, any `n`-th primitive root of unity `ζ` in `K`, and any natural number `n`, if `ζ` is a primitive `n`-th root of unity, then the `n`-th cyclotomic polynomial with coefficients in `K` is equal to the product of the polynomials `(X - C μ)` for each `μ` in the set of primitive `n`-th roots of unity in `K`. In other words, the `n`-th cyclotomic polynomial can be expressed as a product of terms each subtracting a primitive `n`-th root of unity from the polynomial variable `X`.
More concisely: For any commutative ring K that is an integral domain, the n-th cyclotomic polynomial over K, evaluated at the set of its n primitive roots of unity, equals the product of the polynomials (X - ζ) for each primitive n-th root of unity ζ in K.
|
Polynomial.prod_cyclotomic'_eq_X_pow_sub_one
theorem Polynomial.prod_cyclotomic'_eq_X_pow_sub_one :
∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
0 < n → IsPrimitiveRoot ζ n → (n.divisors.prod fun i => Polynomial.cyclotomic' i K) = Polynomial.X ^ n - 1
This theorem states that if there exists a primitive n-th root of unity in a commutative ring domain K, then the product of the modified cyclotomic polynomials of the divisors of n, with coefficients in K, equals the polynomial X raised to the power n minus 1. Here, X is the polynomial variable or indeterminate, and a primitive n-th root of unity is an element that, when raised to the n-th power, gives 1, but does not give 1 for any positive integer power less than n. In other words, the equation `∏ i in Nat.divisors n, cyclotomic' i K = X ^ n - 1` holds true.
More concisely: If a commutative ring domain K contains a primitive n-th root of unity, then the product of the modified cyclotomic polynomials of the divisors of n in K equals X^(n-1) for some indeterminate X.
|
Polynomial.degree_cyclotomic_pos
theorem Polynomial.degree_cyclotomic_pos :
∀ (n : ℕ) (R : Type u_1),
0 < n → ∀ [inst : Ring R] [inst_1 : Nontrivial R], 0 < (Polynomial.cyclotomic n R).degree
This theorem states that for any natural number `n` greater than 0 and for any Ring `R` that is nontrivial, the degree of the `n`-th cyclotomic polynomial with coefficients in `R` is also greater than 0.
More concisely: For any nontrivial ring R and natural number n > 0, the degree of the n-th cyclotomic polynomial over R is positive.
|
Polynomial.unique_int_coeff_of_cycl
theorem Polynomial.unique_int_coeff_of_cycl :
∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] [inst_2 : CharZero K] {ζ : K} {n : ℕ+},
IsPrimitiveRoot ζ ↑n → ∃! P, Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' (↑n) K
This theorem states that if `K` is a commutative ring with zero characteristic and `K` contains a primitive `n`-th root of unity `ζ`, then the `n`-th cyclotomic polynomial with coefficients in `K` originates from a unique polynomial with integer coefficients. This mapping from the polynomial with integer coefficients to the cyclotomic polynomial is done via a ring homomorphism that casts integers to elements of the ring `K`. The existence and uniqueness of such an integer coefficient polynomial is guaranteed by the theorem. The `n`-th cyclotomic polynomial is the product of linear terms `X - μ`, where `μ` ranges over the `n`-th primitive roots of unity in `K`.
More concisely: If `K` is a commutative ring with zero characteristic containing a primitive `n`-th root of unity, then there exists a unique integer polynomial `p` such that the cyclotomic polynomial `Φ_n(X)` in `K[X]` is the image of `p(X)` under the ring homomorphism mapping integers to elements of `K`.
|
Polynomial.cyclotomic_ne_zero
theorem Polynomial.cyclotomic_ne_zero :
∀ (n : ℕ) (R : Type u_1) [inst : Ring R] [inst_1 : Nontrivial R], Polynomial.cyclotomic n R ≠ 0
The theorem `Polynomial.cyclotomic_ne_zero` states that for any natural number `n`, and for any type `R` that forms a nontrivial ring, the `n`-th cyclotomic polynomial with coefficients in `R` is never equal to 0. In other words, given any nontrivial ring, the cyclotomic polynomial of any order in that ring is always non-zero.
More concisely: For any natural number `n` and nontrivial ring `R`, the `n`-th cyclotomic polynomial over `R` is never the zero polynomial.
|
Polynomial.coprime_of_root_cyclotomic
theorem Polynomial.coprime_of_root_cyclotomic :
∀ {n : ℕ},
0 < n →
∀ {p : ℕ} [hprime : Fact p.Prime] {a : ℕ},
(Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a) → a.Coprime p
This theorem states that if a natural number `a` is a root of the `n`-th cyclotomic polynomial with coefficients in the integers modulo a prime number `p`, then `a` and `p` are coprime. More formally, for any positive natural number `n` and any prime number `p`, if `a` is a root of `cyclotomic n (ZMod p)` under the natural number to ZMod `p` ring homomorphism, then `a` is coprime to `p`. In other words, the greatest common divisor of `a` and `p` is 1.
More concisely: If a prime number `p` divides the `n`-th cyclotomic polynomial evaluated at a natural number `a` modulo `p`, then `a` and `p` are coprime.
|
Polynomial.natDegree_cyclotomic
theorem Polynomial.natDegree_cyclotomic :
∀ (n : ℕ) (R : Type u_1) [inst : Ring R] [inst_1 : Nontrivial R],
(Polynomial.cyclotomic n R).natDegree = n.totient
The theorem `Polynomial.natDegree_cyclotomic` states that for any natural number `n` and any type `R` which is a ring and nontrivial (i.e., `R` has at least two distinct elements), the natural degree of the `n`-th cyclotomic polynomial with coefficients in `R` is equal to the Euler's totient function for `n`. Here, the natural degree of a polynomial is a version of the degree of the polynomial that is defined to be a natural number, and the Euler's totient function of a natural number `n` counts the number of natural numbers less than `n` which are coprime with `n`.
More concisely: For any natural number `n` and nontrivial ring `R`, the natural degree of the `n`-th cyclotomic polynomial over `R` equals the Euler's totient function of `n`.
|
Polynomial.cyclotomic'_one
theorem Polynomial.cyclotomic'_one :
∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.cyclotomic' 1 R = Polynomial.X - 1 := by
sorry
The theorem `Polynomial.cyclotomic'_one` states that the first modified cyclotomic polynomial, which is defined with coefficients in a given type `R` (with the structure of a commutative ring and a domain), is equal to the polynomial `X - 1`. This implies that when there is a primitive first root of unity in `R`, the first cyclotomic polynomial is simply `X - 1`.
More concisely: The first modified cyclotomic polynomial over a commutative ring and domain equals `X - 1` if there exists a primitive root of unity in the ring.
|
Polynomial.cyclotomic.proof_1
theorem Polynomial.cyclotomic.proof_1 :
∀ (n : ℕ),
¬n = 0 →
∃ P,
Polynomial.map (Int.castRingHom ℂ) P = Polynomial.cyclotomic' n ℂ ∧
P.degree = (Polynomial.cyclotomic' n ℂ).degree ∧ P.Monic
This theorem states that for any non-zero natural number `n`, there exists a polynomial `P` such that when `P` is mapped across the ring homomorphism from integers to complex numbers, it equals the `n`-th cyclotomic polynomial (in the complex number field), and the degree of `P` equals the degree of the `n`-th cyclotomic polynomial. Additionally, the polynomial `P` is monic, which means its leading coefficient is 1. In other words, there is a monic polynomial with integer coefficients that, upon casting to the complex numbers and measuring degree, behaves like the `n`-th cyclotomic polynomial over the complex numbers.
More concisely: For any natural number `n`, there exists a monic polynomial `P` with integer coefficients of degree `n` that maps to the `n`-th cyclotomic polynomial in the complex numbers under the ring homomorphism from integers to complex numbers.
|
Polynomial.roots_of_cyclotomic
theorem Polynomial.roots_of_cyclotomic :
∀ (n : ℕ) (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R],
(Polynomial.cyclotomic' n R).roots = (primitiveRoots n R).val
The theorem `Polynomial.roots_of_cyclotomic` states that for any natural number `n` and any commutative ring `R` that is also an integral domain, the roots of the modified `n`-th cyclotomic polynomial (denoted as `Polynomial.cyclotomic' n R`) are exactly the primitive `n`-th roots of unity in the ring `R`. In other words, the set of roots of the modified `n`-th cyclotomic polynomial in `R` is precisely the set of elements in `R` that are primitive `n`-th roots of unity.
More concisely: The theorem asserts that the roots of the modified n-th cyclotomic polynomial in an integral domain R are the primitive n-th roots of unity in R.
|
Polynomial.cyclotomic_eq_X_pow_sub_one_div
theorem Polynomial.cyclotomic_eq_X_pow_sub_one_div :
∀ {R : Type u_1} [inst : CommRing R] {n : ℕ},
0 < n →
Polynomial.cyclotomic n R =
(Polynomial.X ^ n - 1).divByMonic (n.properDivisors.prod fun i => Polynomial.cyclotomic i R)
The theorem `Polynomial.cyclotomic_eq_X_pow_sub_one_div` states that for any commutative ring `R` and any positive natural number `n`, the `n`-th cyclotomic polynomial with coefficients in `R` is equal to the polynomial `(X^n - 1)` divided by the product of the cyclotomic polynomials for all proper divisors of `n`. In mathematical terms, for `n` greater than 0, we have the relation: `cyclotomic(n, R) = (X^n - 1) / (∏ i in properDivisors(n), cyclotomic(i, R))`.
More concisely: For any commutative ring R and positive natural number n, the n-th cyclotomic polynomial equals (X^n - 1) divided by the product of the cyclotomic polynomials of all proper divisors of n.
|
Polynomial.map_cyclotomic_int
theorem Polynomial.map_cyclotomic_int :
∀ (n : ℕ) (R : Type u_1) [inst : Ring R],
Polynomial.map (Int.castRingHom R) (Polynomial.cyclotomic n ℤ) = Polynomial.cyclotomic n R
This theorem states that for any natural number `n` and any ring `R`, the `n`-th cyclotomic polynomial with coefficients in `R` is obtained by mapping the `n`-th cyclotomic polynomial with coefficients in the ring of integers `ℤ` across the ring homomorphism from `ℤ` to `R`. This is achieved by using the `Polynomial.map` function with the `Int.castRingHom R` as the ring homomorphism.
More concisely: The `n`-th cyclotomic polynomial over a ring `R` is the image of the `n`-th cyclotomic polynomial over the integers under the ring homomorphism from the integers to `R`.
|
Polynomial.cyclotomic'_two
theorem Polynomial.cyclotomic'_two :
∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R] (p : ℕ) [inst_2 : CharP R p],
p ≠ 2 → Polynomial.cyclotomic' 2 R = Polynomial.X + 1
The theorem `Polynomial.cyclotomic'_two` states that for any commutative ring `R` that is also a domain, and any natural number `p` characteristic of `R`, if `p` is not equal to `2`, then the second modified cyclotomic polynomial over `R` is equal to `X + 1`. This essentially means that the polynomial `X + 1` is a cyclotomic polynomial for `n = 2` in any ring `R` whose characteristic is not `2`. This polynomial represents the minimal polynomial over `R` of a primitive second root of unity, if such a root exists in `R`.
More concisely: For any commutative domain ring R of characteristic not equal to 2, the second modified cyclotomic polynomial over R is equal to X + 1.
|
Polynomial.prod_cyclotomic_eq_X_pow_sub_one
theorem Polynomial.prod_cyclotomic_eq_X_pow_sub_one :
∀ {n : ℕ},
0 < n →
∀ (R : Type u_1) [inst : CommRing R],
(n.divisors.prod fun i => Polynomial.cyclotomic i R) = Polynomial.X ^ n - 1
The theorem `Polynomial.prod_cyclotomic_eq_X_pow_sub_one` asserts that for every positive natural number `n` and for any commutative ring `R`, the product of the `n`-th cyclotomic polynomials with coefficients in `R`, where the product is taken over the divisors of `n`, is equal to the polynomial `X` raised to the power `n` minus `1`. In mathematical terms, this can be written as $\prod_{i \in \text{divisors}(n)} \text{cyclotomic}(i, R) = X^n - 1$. This is a fundamental result in algebraic number theory.
More concisely: The product of the `n`-th cyclotomic polynomials with coefficients in a commutative ring `R`, taken over the divisors of `n`, equals `X` raised to the power of `n` minus `1` in `R[X]`.
|
Polynomial.cyclotomic_prime_pow_eq_geom_sum
theorem Polynomial.cyclotomic_prime_pow_eq_geom_sum :
∀ {R : Type u_1} [inst : CommRing R] {p n : ℕ},
p.Prime → Polynomial.cyclotomic (p ^ (n + 1)) R = (Finset.range p).sum fun i => (Polynomial.X ^ p ^ n) ^ i
The theorem states that if `p ^ k` is a power of a prime number `p`, then the cyclotomic polynomial of order `p ^ (n + 1)` with coefficients in a commutative ring `R` is equal to the geometric series sum of the polynomial `X` raised to the power `p ^ n`, summed over all natural numbers in the range of `p`. In other words, `cyclotomic(p ^ (n + 1), R) = ∑_{i in range(p)} (X ^ (p ^ n)) ^ i`.
More concisely: The cyclotomic polynomial of order p^(n+1) over a commutative ring R is equal to the sum of X raised to the power p^n, over all natural numbers i in the range of p.
|
Polynomial.cyclotomic'.monic
theorem Polynomial.cyclotomic'.monic :
∀ (n : ℕ) (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], (Polynomial.cyclotomic' n R).Monic
The theorem states that for any natural number `n` and any type `R`, given that `R` is a commutative ring and a domain, the modified `n`-th cyclotomic polynomial with coefficients in `R`, is a monic polynomial. In other words, the leading coefficient of this polynomial is 1.
More concisely: For any natural number `n` and commutative ring and domain `R`, the `n`-th cyclotomic polynomial over `R` is a monic polynomial.
|
Polynomial.cyclotomic_coeff_zero
theorem Polynomial.cyclotomic_coeff_zero :
∀ (R : Type u_1) [inst : CommRing R] {n : ℕ}, 1 < n → (Polynomial.cyclotomic n R).coeff 0 = 1
This theorem states that for any commutative ring `R` and a natural number `n` that is greater than 1, the constant term (coefficient of the zero degree term) of the `n`-th cyclotomic polynomial with coefficients in `R` is `1`. In other words, when you evaluate the `n`-th cyclotomic polynomial at zero, the result is `1` provided `n` is at least `2`.
More concisely: For any commutative ring R and natural number n > 1, the constant term of the n-th cyclotomic polynomial is 1.
|
Polynomial.X_pow_sub_one_eq_prod
theorem Polynomial.X_pow_sub_one_eq_prod :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
0 < n →
IsPrimitiveRoot ζ n →
Polynomial.X ^ n - 1 = (Polynomial.nthRootsFinset n R).prod fun ζ => Polynomial.X - Polynomial.C ζ
The theorem `Polynomial.X_pow_sub_one_eq_prod` states that if there is a primitive nth root of unity in a domain `K` (represented by `R`), then the polynomial `X^n - 1` is equal to the product of `(X - μ)`, where `μ` varies over the nth roots of unity. In mathematical terms, if ζ is a primitive nth root of unity in a commutative ring `R` that is also a domain, and `n` is a positive integer, then `X^n - 1` equals the product of `(X - μ)` for each `μ` in the set of nth roots of unity. The roots are represented as a `Finset` in Lean 4. This is essentially a statement of the factorization of `X^n - 1` over a field containing a primitive nth root of unity. This theorem relates polynomial equations, roots of unity, and the factorization of polynomials.
More concisely: Given a domain `R` containing a primitive nth root ζ of unity, `X^n - 1` equals the product of `(X - μ)` for all nth roots of unity μ in `R`.
|
Polynomial.cyclotomic'_splits
theorem Polynomial.cyclotomic'_splits :
∀ {K : Type u_1} [inst : Field K] (n : ℕ), Polynomial.Splits (RingHom.id K) (Polynomial.cyclotomic' n K)
This theorem states that for any field `K` and any natural number `n`, the modified `n`-th cyclotomic polynomial with coefficients in `K` splits. In other words, the `n`-th cyclotomic polynomial is either zero or all of its irreducible factors have degree 1. This is evaluated under the identity ring homomorphism from the field `K` to itself.
More concisely: The `n`-th cyclotomic polynomial over a field `K` splits completely into linear factors.
|
Polynomial.cyclotomic'_eq_X_pow_sub_one_div
theorem Polynomial.cyclotomic'_eq_X_pow_sub_one_div :
∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
0 < n →
IsPrimitiveRoot ζ n →
Polynomial.cyclotomic' n K =
(Polynomial.X ^ n - 1).divByMonic (n.properDivisors.prod fun i => Polynomial.cyclotomic' i K)
The theorem `Polynomial.cyclotomic'_eq_X_pow_sub_one_div` states that given a commutative ring `K` that is also an integral domain and a primitive `n`-th root of unity `ζ` in `K` (where `n` is a positive integer), the modified `n`-th cyclotomic polynomial with coefficients in `K` is equal to the polynomial `(X^n - 1)` divided by the product of the modified cyclotomic polynomials of all proper divisors of `n`. Here, `X` is the variable in the polynomial and `divByMonic` denotes division by a monic polynomial.
More concisely: Given a commutative integral domain `K` and a primitive `n`-th root of unity `ζ` in `K`, the modified `n`-th cyclotomic polynomial equals `(X^n - 1) / (prod of modified cyclotomic polynomials of proper divisors of `n`)`.
|
Polynomial.cyclotomic_prime
theorem Polynomial.cyclotomic_prime :
∀ (R : Type u_1) [inst : Ring R] (p : ℕ) [hp : Fact p.Prime],
Polynomial.cyclotomic p R = (Finset.range p).sum fun i => Polynomial.X ^ i
The theorem `Polynomial.cyclotomic_prime` states that if `p` is a prime number, then the `p`-th cyclotomic polynomial with coefficients in a ring `R` is equal to the sum of `X` raised to the power `i`, for all `i` in the set of natural numbers less than `p`. Here, `X` represents the polynomial variable. In mathematical terms, it can be written as: for a prime number `p`, the `p`-th cyclotomic polynomial is given by $\sum_{i=0}^{p-1} X^i$.
More concisely: For a prime number `p`, the `p`-th cyclotomic polynomial equals the sum of `X` raised to the powers from 0 to `p-1`.
|
Polynomial.int_cyclotomic_spec
theorem Polynomial.int_cyclotomic_spec :
∀ (n : ℕ),
Polynomial.map (Int.castRingHom ℂ) (Polynomial.cyclotomic n ℤ) = Polynomial.cyclotomic' n ℂ ∧
(Polynomial.cyclotomic n ℤ).degree = (Polynomial.cyclotomic' n ℂ).degree ∧ (Polynomial.cyclotomic n ℤ).Monic
The theorem `Polynomial.int_cyclotomic_spec` states that for all natural numbers `n`, three properties hold. First, mapping the `n`-th cyclotomic polynomial with integer coefficients to complex numbers using the integer ring homomorphism is equivalent to the modified `n`-th cyclotomic polynomial with complex coefficients. Second, the degree of the `n`-th cyclotomic polynomial with integer coefficients is equal to the degree of the modified `n`-th cyclotomic polynomial with complex coefficients. Third, the `n`-th cyclotomic polynomial with integer coefficients is a Monic polynomial, meaning its leading coefficient is 1.
More concisely: The `n`-th cyclotomic polynomial with integer coefficients and its modified complex version have equal degrees, coefficients obtained via ring homomorphism are equal, and both are monic polynomials.
|
Polynomial.cyclotomic_one
theorem Polynomial.cyclotomic_one : ∀ (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic 1 R = Polynomial.X - 1 := by
sorry
The theorem `Polynomial.cyclotomic_one` states that, for any type `R` which has a structure of a ring, the first cyclotomic polynomial with coefficients in `R` is `X - 1`. In other words, when you calculate the first cyclotomic polynomial in any ring, this polynomial is equivalent to the polynomial `X - 1`, where `X` is the polynomial variable.
More concisely: The first cyclotomic polynomial over any ring `R` equals `X - 1`.
|
Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius
theorem Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius :
∀ {n : ℕ} (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],
(algebraMap (Polynomial R) (RatFunc R)) (Polynomial.cyclotomic n R) =
n.divisorsAntidiagonal.prod fun i =>
(algebraMap (Polynomial R) (RatFunc R)) (Polynomial.X ^ i.2 - 1) ^ ArithmeticFunction.moebius i.1
The theorem `Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius` states that for any natural number `n` and any commutative ring `R` that is also a domain, the `n`-th cyclotomic polynomial (i.e., a polynomial that divides `X^n - 1` into irreducible factors) with coefficients in `R` can be expressed as a product in the fraction field of the ring of polynomials in `R` with respect to the variable `X`. The product is taken over all pairs `(i.1, i.2)` in the antidiagonal of `n` (pairs `(a, b)` such that `a * b = n`), and each factor is the map into the fraction field of the polynomial `(X^i.2 - 1)` raised to the power of the Möbius function applied to `i.1`. The Möbius function is a number-theoretic function used in the study of prime numbers and arithmetic functions, which assigns to each natural number an integer value depending on the number's prime factorization.
More concisely: For any natural number `n` and commutative domain `R`, the `n`-th cyclotomic polynomial over `R` is equal to the product, in the fraction field of `R[X]`, of the polynomials `(X^i.2 - 1)^μ(i)`, where `(i.1, i.2)` is an antidiagonal pair of `n` and `μ(i.1)` is the Möbius function.
|
Polynomial.cyclotomic_zero
theorem Polynomial.cyclotomic_zero : ∀ (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic 0 R = 1
The theorem `Polynomial.cyclotomic_zero` states that the zeroth cyclotomic polynomial, regardless of the ring `R` over which it is considered, is always equal to `1`. Here, `R` can be any type endowed with a ring structure. Essentially, this theorem asserts a constant value of `1` for the cyclotomic polynomial when the input parameter `n` is zero.
More concisely: The zeroth cyclotomic polynomial equals 1 in any commutative ring.
|
Polynomial.degree_cyclotomic'
theorem Polynomial.degree_cyclotomic' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
IsPrimitiveRoot ζ n → (Polynomial.cyclotomic' n R).degree = ↑n.totient
The theorem `Polynomial.degree_cyclotomic'` states that for any commutative ring `R` that is also an integral domain, for any element `ζ` of `R`, and for any natural number `n`, if `ζ` is a primitive `n`-th root of unity in `R`, then the degree of the `n`-th modified cyclotomic polynomial with coefficients in `R` is equal to the totient function of `n`. The totient function, often denoted as `φ(n)`, counts the number of positive integers up to a given integer `n` that are relatively prime to `n`.
More concisely: For any commutative integral domain R, the degree of the n-th modified cyclotomic polynomial with coefficients in R, evaluated at a primitive n-th root of unity, equals the totient function of n.
|
Polynomial.orderOf_root_cyclotomic_dvd
theorem Polynomial.orderOf_root_cyclotomic_dvd :
∀ {n : ℕ} (hpos : 0 < n) {p : ℕ} [inst : Fact p.Prime] {a : ℕ}
(hroot : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)),
orderOf (ZMod.unitOfCoprime a ⋯) ∣ n
This theorem states that if a natural number `a` is a root of the `n`-th cyclotomic polynomial with coefficients in the integers modulo a prime number `p`, then the multiplicative order of `a` modulo `p` divides `n`. In mathematical terms, if `a` satisfies the equation `cyclotomic(n, ZMod p) = 0`, and the multiplicative order of `a` modulo `p` is the smallest positive integer `m` such that `a^m ≡ 1 (mod p)`, then `m` is a divisor of `n`.
More concisely: If a natural number `a` is a root of the `n`-th cyclotomic polynomial modulo a prime number `p`, then the multiplicative order of `a` modulo `p` divides `n`.
|
Polynomial.int_coeff_of_cyclotomic'
theorem Polynomial.int_coeff_of_cyclotomic' :
∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
IsPrimitiveRoot ζ n →
∃ P,
Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' n K ∧
P.degree = (Polynomial.cyclotomic' n K).degree ∧ P.Monic
The theorem states that, if `K` is a commutative ring with 1 that is also a domain, and there exists a primitive `n`-th root of unity (denoted by `ζ`) in `K`, then there exists a monic polynomial `P` with integer coefficients such that when `P` is mapped from the integers to `K` using the integer casting ring homomorphism, it equals the `n`-th modified cyclotomic polynomial with coefficients in `K`. Additionally, the degree of `P` and the degree of the `n`-th cyclotomic polynomial are the same.
In simpler terms, this theorem is saying that if a certain mathematical condition (specifically, the existence of a primitive `n`-th root of unity) holds in a given ring, then the `n`-th cyclotomic polynomial in that ring can be derived from a polynomial with integer coefficients that has some particular properties (specifically, being monic and having the same degree as the cyclotomic polynomial).
More concisely: Given a commutative ring with 1 that is also a domain `K` and contains a primitive `n`-th root of unity `ζ`, there exists a monic polynomial `P` with integer coefficients in `K` such that `P` is the `n`-th modified cyclotomic polynomial when mapped from the integers to `K` using the integer casting ring homomorphism, and the degrees of `P` and the `n`-th cyclotomic polynomial are equal.
|
Polynomial.X_pow_sub_one_dvd_prod_cyclotomic
theorem Polynomial.X_pow_sub_one_dvd_prod_cyclotomic :
∀ (R : Type u_1) [inst : CommRing R] {n m : ℕ},
0 < n → m ∣ n → m ≠ n → Polynomial.X ^ m - 1 ∣ n.properDivisors.prod fun i => Polynomial.cyclotomic i R
This theorem states that for any commutative ring `R` and natural numbers `n` and `m` such that `0 < n`, `m` is a divisor of `n`, and `m` is not equal to `n`, the polynomial `X^m - 1` divides the product of the `n`-th cyclotomic polynomials over the proper divisors of `n`. Here `X` is the polynomial variable, `Polynomial.cyclotomic i R` represents the `i`-th cyclotomic polynomial with coefficients in `R`, and `n.properDivisors.prod fun i => Polynomial.cyclotomic i R` represents the product of the `n`-th cyclotomic polynomials for each proper divisor `i` of `n`.
More concisely: For any commutative ring `R` and natural numbers `n` and `m` with `0 < n` and `m` a proper divisor of `n`, `X^m - 1` divides the product of the `n`-th cyclotomic polynomials for the proper divisors of `n` in `R`.
|
Polynomial.cyclotomic'_ne_zero
theorem Polynomial.cyclotomic'_ne_zero :
∀ (n : ℕ) (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.cyclotomic' n R ≠ 0
The theorem `Polynomial.cyclotomic'_ne_zero` states that the modified `n`-th cyclotomic polynomial with coefficients in a type `R` (where `R` is a commutative ring and also an integral domain) is always different from zero. This holds for every natural number `n` and for any type `R` that satisfies these ring conditions.
More concisely: For all natural numbers `n` and commutative integral domains `R`, the modified `n`-th cyclotomic polynomial over `R` is never the zero polynomial.
|
Polynomial.natDegree_cyclotomic'
theorem Polynomial.natDegree_cyclotomic' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
IsPrimitiveRoot ζ n → (Polynomial.cyclotomic' n R).natDegree = n.totient
The theorem `Polynomial.natDegree_cyclotomic'` states that for any commutative ring `R` which is also a domain, a primitive `n`-th root of unity `ζ` in `R`, and a natural number `n`, if `ζ` is a primitive root of unity, then the natural degree of the `n`-th modified cyclotomic polynomial with coefficients in `R` is equal to the totient function of `n`. The totient function, denoted as `n.totient`, counts the positive integers up to `n` that are relatively prime to `n`. The modified cyclotomic polynomial is defined as the product of `(X - μ)` for all `μ` belonging to the set of `n`-th primitive roots of unity in `R`.
More concisely: For any commutative domain R, primitive n-th root of unity ζ in R, and natural number n, the degree of the n-th modified cyclotomic polynomial over R is equal to the totient function of n.
|