Polynomial.cyclotomic.irreducible
theorem Polynomial.cyclotomic.irreducible : ∀ {n : ℕ}, 0 < n → Irreducible (Polynomial.cyclotomic n ℤ)
The theorem `Polynomial.cyclotomic.irreducible` states that for any positive natural number `n`, the `n`-th cyclotomic polynomial with integer coefficients is irreducible. In other words, it claims that any cyclotomic polynomial over the integers cannot be factored into the product of two non-unit polynomials.
More concisely: The `n`-th cyclotomic polynomial over the integers is an irreducible polynomial for any positive integer `n`.
|
Polynomial.cyclotomic_eq_minpoly_rat
theorem Polynomial.cyclotomic_eq_minpoly_rat :
∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K},
IsPrimitiveRoot μ n → 0 < n → ∀ [inst_1 : CharZero K], Polynomial.cyclotomic n ℚ = minpoly ℚ μ
The theorem `Polynomial.cyclotomic_eq_minpoly_rat` states that for any natural number `n`, any field `K`, and any element `μ` of `K` such that `μ` is a primitive `n`-th root of unity and `n` is positive, assuming that `K` has characteristic zero, the `n`-th cyclotomic polynomial with coefficients in the rational numbers `ℚ` is equal to the minimal polynomial of `μ` over `ℚ`. In other words, if `μ` is a primitive `n`-th root of unity in a field of characteristic zero, the `n`-th cyclotomic polynomial describes the minimal polynomial relationship that `μ` satisfies over the rationals.
More concisely: For any primitive n-th root of unity μ in a field of characteristic zero, the n-th cyclotomic polynomial is the minimal polynomial of μ over the rational numbers.
|
Polynomial.cyclotomic.irreducible_rat
theorem Polynomial.cyclotomic.irreducible_rat : ∀ {n : ℕ}, 0 < n → Irreducible (Polynomial.cyclotomic n ℚ)
This theorem states that for all natural numbers `n` greater than zero, the `n`-th cyclotomic polynomial with coefficients in the field of rational numbers (ℚ) is irreducible. In mathematical terms, an irreducible polynomial is a non-constant polynomial that cannot be factored into the product of two non-constant polynomials. In this case, the cyclotomic polynomial of any positive natural number `n` is such a polynomial when its coefficients are rational numbers.
More concisely: For every positive natural number `n`, the `n`-th cyclotomic polynomial over the rational numbers is an irreducible polynomial.
|
IsPrimitiveRoot.isRoot_cyclotomic
theorem IsPrimitiveRoot.isRoot_cyclotomic :
∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [inst_1 : IsDomain R],
0 < n → ∀ {μ : R}, IsPrimitiveRoot μ n → (Polynomial.cyclotomic n R).IsRoot μ
This theorem states that for any commutative ring `R` that is also an integral domain, and for any positive integer `n`, any `n`-th primitive root of unity `μ` in `R` is a root of the `n`-th cyclotomic polynomial with coefficients in `R`. In other words, if `μ` is a complex number that is an `n`-th root of unity (meaning that `μ^n = 1`), then the `n`-th cyclotomic polynomial evaluated at `μ` equals zero.
More concisely: For any commutative ring R that is an integral domain and any positive integer n, the n-th primitive root of unity μ in R is a root of the n-th cyclotomic polynomial over R.
|
IsPrimitiveRoot.minpoly_dvd_cyclotomic
theorem IsPrimitiveRoot.minpoly_dvd_cyclotomic :
∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K},
IsPrimitiveRoot μ n → 0 < n → ∀ [inst_1 : CharZero K], minpoly ℤ μ ∣ Polynomial.cyclotomic n ℤ
This theorem states that for any natural number `n` and any field `K` with characteristic zero, if `μ` is a primitive `n`-th root of unity (i.e., `μ` is a root of 1 and its order is `n`), and `n` is positive, then the minimal polynomial of `μ` over the integers divides the `n`-th cyclotomic polynomial with integer coefficients. In other words, there are no integer polynomial factors of the `n`-th cyclotomic polynomial that do not also have `μ` as a root. Here, the minimal polynomial of a number is the monic polynomial of least degree that has the number as a root.
More concisely: For any positive integer `n` and field `K` of characteristic zero, the minimal polynomial of a primitive `n`-th root of unity `μ` in `K` divides the `n`-th cyclotomic polynomial.
|
Polynomial.cyclotomic_injective
theorem Polynomial.cyclotomic_injective :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : CharZero R], Function.Injective fun n => Polynomial.cyclotomic n R
In a commutative ring 'R' with characteristic zero, the function that maps each natural number 'n' to the 'n'-th cyclotomic polynomial with coefficients in 'R' is injective. This means that if two different natural numbers are mapped to the same cyclotomic polynomial, then those two natural numbers must in fact be the same.
More concisely: In a commutative ring of characteristic zero, the map taking natural numbers to their corresponding cyclotomic polynomials is an injection.
|
Polynomial.cyclotomic.isCoprime_rat
theorem Polynomial.cyclotomic.isCoprime_rat :
∀ {n m : ℕ}, n ≠ m → IsCoprime (Polynomial.cyclotomic n ℚ) (Polynomial.cyclotomic m ℚ)
This theorem states that if `n` and `m` are two distinct natural numbers, then the `n`-th and `m`-th cyclotomic polynomials with coefficients in the field of rational numbers are coprime. Being coprime is defined as the existence of two elements (in the field of coefficients) such that their linear combination equals 1. Note that in this context, two polynomials are considered to be coprime if their greatest common divisor is a nonzero constant polynomial.
More concisely: The `n`-th and `m`-th cyclotomic polynomials over the rational numbers are coprime when `n` and `m` are distinct natural numbers.
|
Polynomial.isRoot_cyclotomic_iff
theorem Polynomial.isRoot_cyclotomic_iff :
∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [inst_1 : IsDomain R] [inst_2 : NeZero ↑n] {μ : R},
(Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
The theorem `Polynomial.isRoot_cyclotomic_iff` states the following: for any commutative ring `R`, where `R` is a domain and `n` is a nonzero natural number, a number `μ` is a root of the `n`-th cyclotomic polynomial with coefficients in `R` if and only if `μ` is a primitive root of order `n`. In other words, the number `μ` is a solution to the `n`-th cyclotomic polynomial equation if and only if `μ` is a primitive root with an order of `n`.
More concisely: For a commutative domain R and natural number n, an element μ of R is a root of the n-th cyclotomic polynomial if and only if it is a primitive n-th root in R.
|
IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible
theorem IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible :
∀ {K : Type u_2} [inst : Field K] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : IsDomain R] {μ : R} {n : ℕ}
[inst_3 : Algebra K R],
IsPrimitiveRoot μ n →
Irreducible (Polynomial.cyclotomic n K) → ∀ [inst_4 : NeZero ↑n], Polynomial.cyclotomic n K = minpoly K μ
This theorem states that for any natural number `n`, any field `K`, any commutative ring `R`, and any element `μ` of `R`, if `μ` is a primitive root of `n`, and the `n`-th cyclotomic polynomial with coefficients in `K` is irreducible, then the `n`-th cyclotomic polynomial with coefficients in `K` is equal to the minimal polynomial of `μ` over `K`, provided that `n` is not zero. The statement assumes that `R` is a domain, and that `K` is an algebra over `R`.
More concisely: For any natural number `n` not equal to zero, if `μ` is a primitive root of unity of order `n` over a field `K`, and the `n`-th cyclotomic polynomial is irreducible over `K`, then it is the minimal polynomial of `μ` over `K`.
|
Polynomial.isRoot_cyclotomic_iff_charZero
theorem Polynomial.isRoot_cyclotomic_iff_charZero :
∀ {n : ℕ} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CharZero R] {μ : R},
0 < n → ((Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n)
This theorem states that given a commutative ring `R` with a characteristic of zero, a number `μ` is a root of the `n`-th cyclotomic polynomial with coefficients in `R` if and only if `μ` is a primitive `n`-th root of unity. This is conditional on `n` being a positive natural number. In mathematical terms, it asserts that for a nonzero natural number `n`, `μ` is a root of the `n`-th cyclotomic polynomial defined over `R` if and only if `μ` is a root of unity of order `n`.
More concisely: Given a commutative ring `R` with characteristic zero, a natural number `n`, and an element `μ` in `R`, `μ` is a root of the `n`-th cyclotomic polynomial over `R` if and only if `μ` is a primitive `n`-th root of unity.
|
Polynomial.cyclotomic_eq_minpoly
theorem Polynomial.cyclotomic_eq_minpoly :
∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K},
IsPrimitiveRoot μ n → 0 < n → ∀ [inst_1 : CharZero K], Polynomial.cyclotomic n ℤ = minpoly ℤ μ
The theorem `Polynomial.cyclotomic_eq_minpoly` states that for any positive natural number `n`, any field `K` with characteristic zero, and any value `μ` in `K` that is a primitive `n`-th root of unity, the `n`-th cyclotomic polynomial with integer coefficients (`Polynomial.cyclotomic n ℤ`) is equal to the minimal polynomial of `μ` over the integers (`minpoly ℤ μ`).
More concisely: For any positive integer `n` and any primitive `n`-th root of unity `μ` in a field `K` of characteristic zero, the `n`-th cyclotomic polynomial with integer coefficients equals the minimal polynomial of `μ` over the integers.
|