IsPrimitiveRoot.totient_le_degree_minpoly
theorem IsPrimitiveRoot.totient_le_degree_minpoly :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n → ∀ [inst_1 : IsDomain K] [inst_2 : CharZero K], n.totient ≤ (minpoly ℤ μ).natDegree
This theorem states that for a given positive integer `n`, a type `K` that forms a commutative ring, and an element `μ` of `K` that is a primitive root of `n`, given that `K` is also a domain and has characteristic zero, the totient of `n` (i.e., the number of integers less than `n` that are coprime with `n`) is less than or equal to the natural degree of the minimal polynomial of `μ` over the integers.
More concisely: The number of integers less than a positive integer `n` coprime to `n` is bounded above by the degree of the minimal polynomial of a primitive root of `n` in a commutative ring `K` of characteristic zero and with identity.
|
IsPrimitiveRoot.minpoly_eq_pow
theorem IsPrimitiveRoot.minpoly_eq_pow :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n →
∀ [inst_1 : IsDomain K] [inst_2 : CharZero K] {p : ℕ} [hprime : Fact p.Prime],
¬p ∣ n → minpoly ℤ μ = minpoly ℤ (μ ^ p)
The theorem `IsPrimitiveRoot.minpoly_eq_pow` states that given a natural number `n`, a commutative ring `K`, and an element `μ` of `K` which is a primitive `n`-th root of unity, if `K` is a domain with characteristic zero, and `p` is a prime number which does not divide `n`, then the minimal polynomial over the integers of `μ` is equal to the minimal polynomial over the integers of `μ` to the power of `p`.
More concisely: If `n` is a natural number, `K` is a characteristic-zero domain, `p` is a prime number not dividing `n`, and `μ` is a primitive `n`-th root of unity in `K`, then the minimal polynomial of `μ` over the integers is equal to the minimal polynomial of `μ^p` over the integers.
|
IsPrimitiveRoot.is_roots_of_minpoly
theorem IsPrimitiveRoot.is_roots_of_minpoly :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n →
∀ [inst_1 : IsDomain K] [inst_2 : CharZero K] [inst_3 : DecidableEq K],
primitiveRoots n K ⊆ (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
This theorem asserts that if `μ` is a primitive `n`-th root of unity in a commutative ring `K` (with the ring `K` being an integral domain and having characteristic zero), then the set of all primitive `n`-th roots of unity in `K` is a subset of the roots of the minimal polynomial of `μ` over the integers, when this polynomial is viewed as a polynomial over `K` via the natural ring homomorphism from the integers to `K`. In other words, every primitive `n`-th root of unity in `K` is also a root of the minimal polynomial of any primitive `n`-th root of unity `μ`.
More concisely: If `μ` is a primitive n-th root of unity in the integral domain K of characteristic zero, then the set of all primitive n-th roots of unity in K is included in the roots of the minimal polynomial of `μ` viewed as a polynomial over K.
|
IsPrimitiveRoot.squarefree_minpoly_mod
theorem IsPrimitiveRoot.squarefree_minpoly_mod :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n →
∀ [inst_1 : IsDomain K] [inst_2 : CharZero K] {p : ℕ} [inst_3 : Fact p.Prime],
¬p ∣ n → Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
The theorem `IsPrimitiveRoot.squarefree_minpoly_mod` states that for any natural number `n`, any type `K` that is a commutative ring, and any `μ` of type `K` which is a primitive root of `n`, given that `K` is a domain and has characteristic zero, and for any prime number `p` that does not divide `n`, the reduction modulo `p` of the minimal polynomial of `μ` is squarefree. In other words, the only squares that divide the polynomial obtained by reducing the minimal polynomial of `μ` modulo `p`, are the squares of units. This is a property in the field of Number Theory, specifically about roots of unity and their minimal polynomials.
More concisely: Given a natural number `n`, a commutative domain `K` of characteristic zero, and a primitive root `μ` of `n` in `K`, for any prime `p` not dividing `n`, the reduced minimal polynomial of `μ` modulo `p` is squarefree.
|
IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one
theorem IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n → ∀ [inst_1 : IsDomain K] [inst_2 : CharZero K], minpoly ℤ μ ∣ Polynomial.X ^ n - 1
This theorem states that for any natural number `n` and any type `K` with an instance of a commutative ring, given an element `μ` of `K` that is a primitive root of `n`, and assuming `K` is a domain and its characteristic is zero, then the minimal polynomial of `μ` over the integers (ℤ) divides the polynomial `X^n - 1`. In other words, `X^n - 1` is a multiple of the minimal polynomial of `μ`. Here `X` is the polynomial variable and '^' denotes exponentiation.
More concisely: For any natural number `n`, and commutative ring `K` with characteristic zero and an element `μ` being a primitive root of `n` in `K`, the minimal polynomial of `μ` over the integers (ℤ) divides `X^n - 1` in `K[X]`.
|
IsPrimitiveRoot.minpoly_eq_pow_coprime
theorem IsPrimitiveRoot.minpoly_eq_pow_coprime :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n →
∀ [inst_1 : IsDomain K] [inst_2 : CharZero K] {m : ℕ}, m.Coprime n → minpoly ℤ μ = minpoly ℤ (μ ^ m)
This theorem states that for any natural number `n` and any type `K` that is a commutative ring, if `μ` is a primitive `n`-th root of unity, then for any `m` that is coprime with `n`, the minimal polynomial of `μ` is equal to the minimal polynomial of `μ` to the power `m`. Here, the assumption is that `K` is a domain and has characteristic zero.
More concisely: For any commutative ring `K` of characteristic zero and any natural number `n`, if `μ` is a primitive `n`-th root of unity in `K`, then the minimal polynomial of `μ` and `μ^m` are equal for any `m` coprime to `n`.
|
IsPrimitiveRoot.isIntegral
theorem IsPrimitiveRoot.isIntegral :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K}, IsPrimitiveRoot μ n → 0 < n → IsIntegral ℤ μ
The theorem `IsPrimitiveRoot.isIntegral` asserts that for any natural number `n` and any type `K` that forms a commutative ring, if `μ` is a primitive `n`th root in `K`, and `n` is greater than zero, then `μ` is integral over the integers (`ℤ`). In other words, `μ` is a root of some monic polynomial with integer coefficients.
More concisely: For any natural number `n` and commutative ring `K`, if `μ` is a primitive `n`th root in `K`, then `μ` is a root of some monic polynomial with integer coefficients in `K[X]`.
|
IsPrimitiveRoot.pow_isRoot_minpoly
theorem IsPrimitiveRoot.pow_isRoot_minpoly :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n →
∀ [inst_1 : IsDomain K] [inst_2 : CharZero K] {m : ℕ},
m.Coprime n → (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)
This theorem states that given a natural number `n` and a commutative ring `K`, if `μ` is a primitive `n`-th root of unity in `K`, then for any natural number `m` that is coprime with `n`, the minimal polynomial of `μ` evaluated at `μ ^ m` equals zero. In other words, `μ ^ m` is a root of the minimal polynomial of `μ`. This evaluation process consists of mapping the coefficients of the polynomial from integers to elements of the ring `K` using the `Int.castRingHom K` function.
More concisely: Given a commutative ring K and a primitive n-th root μ of unity in K, for any natural number m coprime to n, the minimal polynomial of μ evaluates to zero at μ^m.
|
IsPrimitiveRoot.separable_minpoly_mod
theorem IsPrimitiveRoot.separable_minpoly_mod :
∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
IsPrimitiveRoot μ n →
∀ [inst_1 : IsDomain K] [inst_2 : CharZero K] {p : ℕ} [inst_3 : Fact p.Prime],
¬p ∣ n → (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable
The theorem `IsPrimitiveRoot.separable_minpoly_mod` states that for any natural number `n`, commutative ring `K`, and element `μ` of `K` that is a primitive root of `n`, assuming `K` is a field and its characteristic is zero, and for any prime number `p` which does not divide `n`, the result of mapping the minimal polynomial of `μ` over integers, through the ring homomorphism from integers to integers modulo `p`, is a separable polynomial. In other words, after reducing the minimal polynomial of a root of unity mod `p`, the resulting polynomial does not have any multiple roots in the field of integers modulo `p`.
More concisely: If `n` is a natural number, `K` is a field of characteristic zero, `μ` is a primitive root of `n` in `K`, and `p` is a prime number not dividing `n`, then the reduction of the minimal polynomial of `μ` over the integers, through the ring homomorphism from integers to integers modulo `p`, is a separable polynomial.
|