IsPrimitiveRoot.coe_units_iff
theorem IsPrimitiveRoot.coe_units_iff :
∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : Mˣ}, IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
This theorem states that for any type `M` which forms a commutative monoid, for any natural number `k`, and for any unit `ζ` in `M`, `ζ` is a primitive root of `k` if and only if the coercion of `ζ` is also a primitive root of `k`. Here, a primitive root of `k` is an element which, when repeatedly multiplied by itself `k` times, yields 1, but does not yield 1 when multiplied by itself fewer than `k` times.
More concisely: For any commutative monoid type `M` and unit `ζ` in `M`, `ζ` is a primitive root of a natural number `k` if and only if the coercion of `ζ` is a primitive root of `k`.
|
IsPrimitiveRoot.pow_sub_one_eq
theorem IsPrimitiveRoot.pow_sub_one_eq :
∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R},
IsPrimitiveRoot ζ k → 1 < k → ζ ^ k.pred = -(Finset.range k.pred).sum fun i => ζ ^ i
The theorem states that for any commutative ring `R` which is also an integral domain, any natural number `k` greater than `1`, and any `ζ` in `R` which is a primitive root of `k`, the `k-1`th power of `ζ` equals the negation of the sum of the `i`th powers of `ζ` for all `i` in the set of natural numbers less than `k-1`. In mathematical notation, if `ζ` is a primitive root of `k` in a commutative ring `R` that is also an integral domain and `k > 1`, then `ζ^(k-1) = -∑(i=0)^(k-2) ζ^i`.
More concisely: For any commutative integral domain `R` and primitive root `ζ` of natural number `k` greater than 1 in `R`, `ζ^(k-1) = -∑(i=0)^(k-2) ζ^i`.
|
IsPrimitiveRoot.nthRoots_eq
theorem IsPrimitiveRoot.nthRoots_eq :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ} {ζ : R},
IsPrimitiveRoot ζ n →
∀ {α a : R}, α ^ n = a → Polynomial.nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)
This theorem states that for any commutative ring `R` that is also a domain, given any natural number `n` and any element `ζ` of `R` that is a primitive `n`th root, and for any elements `α` and `a` of `R` such that `α` to the power of `n` equals `a`, the `n`th roots of `a` (solutions to `x^n = a`) are exactly the elements of the form `ζ^x * α` for `x` in the range from `0` to `n-1`. This essentially ties together the concepts of primitive roots, polynomial roots, and ranges in the context of commutative rings.
More concisely: For any commutative domain `R`, any primitive `n`th root `ζ` in `R`, and any `a` in `R` with `α^n = a`, the `n` roots of `a` are `{ζ^x * α | x <- [0, n-1]}`.
|
Mathlib.RingTheory.RootsOfUnity.Basic._auxLemma.1
theorem Mathlib.RingTheory.RootsOfUnity.Basic._auxLemma.1 :
∀ {M : Type u_1} [inst : CommMonoid M] (k : ℕ+) (ζ : Mˣ), (ζ ∈ rootsOfUnity k M) = (ζ ^ ↑k = 1)
This theorem states that for any type `M` with a commutative monoid structure, any positive natural number `k`, and any element `ζ` of the multiplicative group of `M`, `ζ` is in the roots of unity of `k` in `M` if and only if `ζ` to the power of `k` equals 1. In mathematical notation, this is saying that for any ζ in the multiplicative group of a commutative monoid M and a positive integer k, ζ is a k-th root of unity in M if and only if ζ^k = 1.
More concisely: A commutative monoid element ζ is a root of unity of order k if and only if ζ^k = 1.
|
IsPrimitiveRoot.pow
theorem IsPrimitiveRoot.pow :
∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {n a b : ℕ},
0 < n → IsPrimitiveRoot ζ n → n = a * b → IsPrimitiveRoot (ζ ^ a) b
This theorem states that if ζ is an n-th primitive root of unity in a commutative monoid `M` and `b` divides `n` (with `n` being the product of `a` and `b`), then there exists a `b`-th primitive root of unity in `M` which is the `a`-th power of ζ. Here, `n` must be a positive natural number. Essentially, the theorem describes a property of primitive roots of unity which allows us to find a `b`-th primitive root from an `n`-th primitive root, given certain divisibility conditions.
More concisely: If `ζ` is an `n`-th root of unity in a commutative monoid `M` and `b` divides `n`, then there exists a `b`-th root of unity in `M` that is the `a`-th power of `ζ`.
|
IsPrimitiveRoot.disjoint
theorem IsPrimitiveRoot.disjoint :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {k l : ℕ},
k ≠ l → Disjoint (primitiveRoots k R) (primitiveRoots l R)
This theorem states that for any type `R`, which is a commutative ring and an integral domain, and for any two distinct natural numbers `k` and `l`, the sets of `k`-th primitive roots of unity and `l`-th primitive roots of unity (in `R`) are pairwise disjoint. In other words, there is no common `k`-th and `l`-th primitive root of unity in the integral domain `R` if `k` and `l` are different. This is formalized in Lean 4 using the `Disjoint` predicate, which says that the greatest lower bound (infimum) of two elements in a lattice is the bottom element of the lattice. In the context of sets, this means that the sets have no element in common.
More concisely: For any commutative ring and integral domain R, the sets of k-th and l-th primitive roots of unity in R are disjoint for distinct natural numbers k and l.
|
Mathlib.RingTheory.RootsOfUnity.Basic._auxLemma.13
theorem Mathlib.RingTheory.RootsOfUnity.Basic._auxLemma.13 :
∀ {M : Type u_1} [inst : CommMonoid M] (ζ : M) (k : ℕ),
IsPrimitiveRoot ζ k = (ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l)
This theorem states that for any commutative monoid `M` and any element `ζ` of `M`, `ζ` is a primitive root of order `k` if and only if `ζ` raised to the `k`th power equals one and for any natural number `l`, if `ζ` raised to the `l`th power equals one, then `k` divides `l`. In simpler terms, a number is a primitive root of a certain order if it cycles back to 1 after that many steps and any other power that brings it to 1 must be a multiple of that order.
More concisely: A commutative monoid element `ζ` is a primitive root of order `k` if and only if `ζ^k = 1` and `k` divides `l` for all `l` such that `ζ^l = 1`.
|
IsPrimitiveRoot.zpowers_eq
theorem IsPrimitiveRoot.zpowers_eq :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {k : ℕ+} {ζ : Rˣ},
IsPrimitiveRoot ζ ↑k → Subgroup.zpowers ζ = rootsOfUnity k R
This theorem states that for any commutative ring `R` that is also an integral domain, and for any positive natural number `k` and unit `ζ` of `R`, if `ζ` is a primitive root of `k` (i.e., `ζ` to the power of `k` equals `1` and `ζ` is not a root of any smaller natural number), then the subgroup generated by the powers of `ζ` is equal to the subgroup of `R`'s units that are roots of unity of order `k` (i.e., elements `m` of the multiplicative group `Mˣ` such that `m` to the power `k` equals `1`).
More concisely: For any commutative ring R that is an integral domain, if positive natural number k has a primitive root ζ in R, then the subgroup of R generated by {ζ^n | n ∈ ℕ} equals the subgroup of R's units that are roots of unity of order k.
|
Mathlib.RingTheory.RootsOfUnity.Basic._auxLemma.4
theorem Mathlib.RingTheory.RootsOfUnity.Basic._auxLemma.4 :
∀ {α : Type u} [inst : Monoid α] {a b : αˣ}, (a = b) = (↑a = ↑b)
This theorem, from the RingTheory.RootsOfUnity.Basic module in Mathlib, states that for any type `α` that has a structure of a monoid, the equality of two units (elements with a multiplicative inverse) `a` and `b` is equivalent to the equality of their corresponding elements in `α`. In other words, two units `a` and `b` are equal if and only if their coercions to `α` are equal.
More concisely: For any monoid `α`, two of its units `a` and `b` are equal if and only if their coercions to `α` are equal.
|
IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots'
theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots' :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ+},
IsPrimitiveRoot ζ ↑n → Polynomial.nthRootsFinset (↑n) R = (↑n).divisors.biUnion fun i => primitiveRoots i R
The theorem `IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots'` states that if ζ is a primitive nth root of unity in a commutative ring R that is also an integral domain, then the finset of nth roots of unity is equal to the union of the finsets of primitive ith roots of unity for each i that divides n. This holds for any natural number n, not just positive natural numbers. This is a generalization of the theorem `nthRoots_one_eq_bUnion_primitive_roots` which applies only to positive natural numbers.
More concisely: If ζ is a primitive nth root of unity in an integral domain R, then the set of nth roots of unity equals the union of the sets of primitive ith roots of unity for all i dividing n.
|
IsPrimitiveRoot.card_nthRoots_one
theorem IsPrimitiveRoot.card_nthRoots_one :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
IsPrimitiveRoot ζ n → Multiset.card (Polynomial.nthRoots n 1) = n
The theorem `IsPrimitiveRoot.card_nthRoots_one` states that for any commutative ring `R` that is also an integral domain, if `ζ` is a primitive nth root of unity in `R` (meaning ζ^n = 1 and ζ^k ≠ 1 for any positive integer `k` less than `n`), then the cardinality (or size) of the multiset of all nth roots of 1 in `R` is exactly `n`. In other words, if there is a primitive nth root of unity in `R`, there are exactly `n` distinct solutions to the equation x^n = 1 in `R`.
More concisely: For any commutative integral domain R, the number of distinct n-th roots of 1 in R is exactly n if and only if there exists a primitive n-th root of unity in R.
|
mem_primitiveRoots
theorem mem_primitiveRoots :
∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R},
0 < k → (ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k)
The theorem `mem_primitiveRoots` asserts that for any type `R` that is a commutative ring and an integral domain, and any natural number `k` that is greater than 0, an element `ζ` belongs to the set of `k`-th primitive roots of unity in `R` if and only if `ζ` is a primitive `k`-th root of unity. In mathematical terms, this theorem establishes that an element is a primitive `k`-th root of unity in an integral domain if it satisfies the properties defined in `IsPrimitiveRoot ζ k`.
More concisely: In an integral domain R, an element ζ is a k-th primitive root of unity if and only if it is a primitive k-th root of unity in R.
|
mem_rootsOfUnity
theorem mem_rootsOfUnity :
∀ {M : Type u_1} [inst : CommMonoid M] (k : ℕ+) (ζ : Mˣ), ζ ∈ rootsOfUnity k M ↔ ζ ^ ↑k = 1
This theorem states that for any commutative monoid `M` and any element `ζ` in the multiplicative group of `M`, `ζ` is a member of the roots of unity of order `k` in `M` if and only if `ζ` raised to the power `k` equals 1. In other words, an element belongs to the `k`-th roots of unity in a given commutative monoid if it satisfies the property that its `k`-th power equals the multiplicative identity.
More concisely: An element `ζ` in a commutative monoid `M` is a `k`-th root of unity if and only if `ζ^k = 1`.
|
IsPrimitiveRoot.eq_pow_of_pow_eq_one
theorem IsPrimitiveRoot.eq_pow_of_pow_eq_one :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {k : ℕ} {ζ ξ : R},
IsPrimitiveRoot ζ k → ξ ^ k = 1 → 0 < k → ∃ i < k, ζ ^ i = ξ
This theorem states that for any commutative ring `R` that is also a domain, given any natural number `k`, and any two elements `ζ` and `ξ` of `R`, if `ζ` is a primitive root of `k` and `ξ` raised to the power of `k` equals 1, and `k` is greater than 0, then there exists a natural number `i` less than `k` such that `ζ` raised to the power of `i` equals `ξ`. In mathematical language, if $\zeta$ is a primitive $k^{th}$ root of unity in a domain $R$ and $\xi$ raised to the power of $k$ equals 1 (where $k > 0$), there exists an integer $i < k$ such that $\zeta^i = \xi$.
More concisely: Given a commutative domain R and natural number k, if ζ is a primitive k-th root of unity in R and ξ = ζ^k = 1, then there exists an integer i < k such that ζ^i = ξ.
|
IsPrimitiveRoot.map_of_injective
theorem IsPrimitiveRoot.map_of_injective :
∀ {M : Type u_1} {N : Type u_2} {F : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {k : ℕ} {ζ : M} {f : F}
[inst_2 : FunLike F M N] [inst_3 : MonoidHomClass F M N],
IsPrimitiveRoot ζ k → Function.Injective ⇑f → IsPrimitiveRoot (f ζ) k
This theorem states that if `ζ` is a primitive root of order `k` in a commutative monoid `M`, and `f` is an injective function that is a monoid homomorphism from `M` to another commutative monoid `N`, then the image of `ζ` under `f` is a primitive root of order `k` in `N`.
In other words, the property of being a primitive root is preserved under the injective homomorphism `f`.
More concisely: If `ζ` is a primitive root of order `k` in a commutative monoid `M` and `f` is an injective homomorphism from `M` to a commutative monoid `N`, then `f(ζ)` is a primitive root of order `k` in `N`.
|
IsPrimitiveRoot.geom_sum_eq_zero
theorem IsPrimitiveRoot.geom_sum_eq_zero :
∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R},
IsPrimitiveRoot ζ k → 1 < k → ((Finset.range k).sum fun i => ζ ^ i) = 0
The theorem `IsPrimitiveRoot.geom_sum_eq_zero` states that for any commutative ring `R` which is also an integral domain, any natural number `k` such that `1 < k`, and any element `ζ` of `R` that is a primitive kth root of unity, the sum of the kth powers of `ζ` for all natural numbers in the range `k` equals zero. In mathematical terms, if `ζ` is a primitive kth root of unity in the commutative ring `R`, then the sum from `i = 0` to `k-1` of `ζ` to the power of `i` is zero.
More concisely: For any commutative integral domain `R` and a primitive `k`th root of unity `ζ` in `R` with `1 < k`, the sum of `ζ` raised to the power of each natural number in the range `0` to `k-1` equals zero.
|
IsPrimitiveRoot.pow_iff_coprime
theorem IsPrimitiveRoot.pow_iff_coprime :
∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
IsPrimitiveRoot ζ k → 0 < k → ∀ (i : ℕ), IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k
The theorem `IsPrimitiveRoot.pow_iff_coprime` states that for any type `M` that has a commutative monoid structure, for any natural number `k`, and for any element `ζ` of `M`, if `ζ` is a primitive root of `k` and `k` is positive, then for any natural number `i`, `ζ` raised to the power `i` is a primitive root of `k` if and only if `i` and `k` are coprime, i.e., their greatest common divisor is 1.
More concisely: For any commutative monoid M, integer k > 0, and primitive root ζ of k in M, i and k are coprime if and only if ζ^i is a primitive root of k.
|
IsPrimitiveRoot.eq_neg_one_of_two_right
theorem IsPrimitiveRoot.eq_neg_one_of_two_right :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : NoZeroDivisors R] {ζ : R}, IsPrimitiveRoot ζ 2 → ζ = -1
This theorem states that for any commutative ring `R` with no zero divisors, if `ζ` is a primitive root of order 2 (which means `ζ` raised to the power of 2 equals 1), then `ζ` must be equal to `-1`. This is because the only two complex roots of the equation $x^2 = 1$ are `1` and `-1`, and by the nature of `ζ` being a "primitive root" of order `2`, it cannot be `1`. Thus, it must be `-1`.
More concisely: In a commutative ring with no zero divisors, a primitive root of order 2 equals -1.
|
IsPrimitiveRoot.nthRoots_one_nodup
theorem IsPrimitiveRoot.nthRoots_one_nodup :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
IsPrimitiveRoot ζ n → (Polynomial.nthRoots n 1).Nodup
The theorem `IsPrimitiveRoot.nthRoots_one_nodup` states that for any commutative ring `R` which is also an integral domain, for any element `ζ` in `R` and for any natural number `n`, if `ζ` is a primitive root of unity of order `n` then the multiset of `n`-th roots of unity in `R`, computed by the function `Polynomial.nthRoots`, contains no duplicate elements. In other words, if `ζ^n = 1` and `ζ` is a primitive root of unity, then each `n`-th root of unity in `R` is unique.
More concisely: In a commutative integral domain, a primitive root of unity of order n in R has exactly n distinct n-th roots.
|
IsPrimitiveRoot.isUnit
theorem IsPrimitiveRoot.isUnit :
∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → 0 < k → IsUnit ζ
This theorem states that for any commutative monoid `M`, any natural number `k` and any element `ζ` of `M`, if `ζ` is a primitive root of order `k` and `k` is a positive number, then `ζ` is a unit of `M`. In other words, if `ζ` is an element of `M` such that raising `ζ` to the power `k` gives the identity element, and `k` is positive, then there exists an inverse of `ζ` in `M`.
More concisely: If `ζ` is a primitive root of order `k` in a commutative monoid `M` with `k` being a positive natural number, then `ζ` is a unit in `M` with an inverse.
|
IsPrimitiveRoot.unique
theorem IsPrimitiveRoot.unique :
∀ {M : Type u_1} [inst : CommMonoid M] {k l : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → IsPrimitiveRoot ζ l → k = l := by
sorry
This theorem states that for any type `M` that is a commutative monoid and any natural numbers `k` and `l`, if `ζ` is a primitive root of both `k` and `l`, then `k` must be equal to `l`. In other words, a primitive root uniquely identifies the order of the group in a commutative monoid.
More concisely: In a commutative monoid, if a primitive root exists for both natural numbers `k` and `l`, then `k` equals `l`.
|
IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots
theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
IsPrimitiveRoot ζ n → Polynomial.nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R
The theorem `IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots` states that for a given commutative ring `R` and a positive integer `n`, if there is a primitive `n`th root of unity in `R`, denoted as `ζ`, then the set of all `n`th roots of unity in `R` (as a Finset) is equal to the union of the sets of primitive `i`th roots of unity in `R` for every `i` that divides `n`.
Practically, this theorem provides a breakdown of the `n`th roots of unity into their primitive components, where primitive roots are those that generate all the `n`th roots of unity when raised to different powers.
More concisely: If a commutative ring `R` has a primitive `n`th root of unity `ζ`, then the set of all `n`th roots of unity in `R` equals the union of the sets of primitive `i`th roots of unity in `R` for all divisors `i` of `n`.
|
IsPrimitiveRoot.pow_ne_one_of_pos_of_lt
theorem IsPrimitiveRoot.pow_ne_one_of_pos_of_lt :
∀ {M : Type u_1} [inst : CommMonoid M] {k l : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → 0 < l → l < k → ζ ^ l ≠ 1 := by
sorry
This theorem states that for any type 'M' that is a commutative monoid, given two natural numbers 'l' and 'k', and an element 'ζ' of 'M' that is a primitive root of 'k', if 'l' is positive and less than 'k', then the 'l'-th power of 'ζ' is not equal to one. In mathematical terms, if ζ is a primitive root of order 'k', then any power 'l' of ζ, where 0 < l < k, is not one.
More concisely: For any commutative monoid M and primitive root ζ of order k in M, if l is a positive natural number less than k, then ζ^l ≠ 1.
|
IsPrimitiveRoot.iff_def
theorem IsPrimitiveRoot.iff_def :
∀ {M : Type u_1} [inst : CommMonoid M] (ζ : M) (k : ℕ),
IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
This theorem states that for any type `M` that forms a commutative monoid and any element `ζ` of `M` and natural number `k`, `ζ` is a primitive root of `k` if and only if `ζ` to the power of `k` equals 1 and for all natural numbers `l`, if `ζ` to the power of `l` equals 1, then `k` divides `l`. Essentially, it defines a primitive root within the context of a commutative monoid.
More concisely: A commutative monoid element `ζ` is a primitive root of natural number `k` if and only if `ζ^k = 1` and for all natural numbers `l` with `ζ^l = 1`, `k` divides `l`.
|
IsPrimitiveRoot.eq_orderOf
theorem IsPrimitiveRoot.eq_orderOf :
∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → k = orderOf ζ
This theorem states that for any type `M` that is a commutative monoid, given a natural number `k` and an element `ζ` of `M`, if `ζ` is a primitive root of `k`, then `k` is equal to the order of `ζ`. Here, a primitive root of `k` is an element `ζ` such that `ζ` to the power of `k` is equal to 1, and the order of an element `ζ` is the smallest natural number `n` such that `ζ` to the power of `n` is equal to 1. If no such `n` exists, the order of `ζ` is defined to be 0.
More concisely: For any commutative monoid `M` and element `ζ` of `M`, if `ζ` is a primitive root of the natural number `k`, then the order of `ζ` equals `k`.
|
IsPrimitiveRoot.pow_of_coprime
theorem IsPrimitiveRoot.pow_of_coprime :
∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
IsPrimitiveRoot ζ k → ∀ (i : ℕ), i.Coprime k → IsPrimitiveRoot (ζ ^ i) k
This theorem states that for any type `M` with a commutative monoid structure, given any natural number `k` and any element `ζ` of type `M` that is a primitive root of `k`, if `i` is a natural number that is coprime with `k` (i.e., the greatest common divisor of `i` and `k` is 1), then `ζ` to the power `i` is also a primitive root of `k`.
More concisely: If `M` is a commutative monoid with an element `ζ` that is a primitive root of natural number `k`, and `i` is a natural number coprime to `k`, then `ζ^i` is also a primitive root of `k`.
|
IsPrimitiveRoot.orderOf
theorem IsPrimitiveRoot.orderOf : ∀ {M : Type u_1} [inst : CommMonoid M] (ζ : M), IsPrimitiveRoot ζ (orderOf ζ) := by
sorry
This theorem states that for any type `M` that is a Commutative Monoid, for any element `ζ` from `M`, `ζ` is a primitive root of its own order. In mathematical terms, if `orderOf ζ` is `n`, that means `ζ^n = 1` and `n` is the smallest such positive integer. The primitive root definition here is a generalization of the concept from number theory, which in this context means that `ζ` generates all the `n`-th roots of unity in the monoid `M` under multiplication.
More concisely: For any commutative monoid M and any element ζ in M of finite order n, ζ is a primitive root of unity of order n, i.e., it generates all n-th roots of unity in M under multiplication.
|
IsPrimitiveRoot.card_primitiveRoots
theorem IsPrimitiveRoot.card_primitiveRoots :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {k : ℕ},
IsPrimitiveRoot ζ k → (primitiveRoots k R).card = k.totient
This theorem states that for any integral domain `R` that has a `k`-th root of unity, denoted as `ζ`, where `ζ` is a primitive root of `k`, the number of primitive `k`-th roots of unity in `R` is equal to the Euler's totient function of `k`. In other words, if `ζ` is a primitive `k`-th root of unity in an integral domain `R`, then `R` contains exactly `φ(k)` such primitive roots, where `φ` is the Euler's totient function. This function `φ(k)` counts the number of integers strictly less than `k` that are coprime with `k`.
More concisely: In an integral domain with a primitive k-th root of unity, the number of such roots is equal to the Euler totient function of k.
|
primitiveRoots_zero
theorem primitiveRoots_zero : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R], primitiveRoots 0 R = ∅ := by
sorry
The theorem `primitiveRoots_zero` states that for any type `R` that is an integral domain with a commutative ring structure, the set of 0-th primitive roots of unity in `R` is empty. In other words, there are no 0-th primitive roots of unity in an integral domain.
More concisely: In any integral domain, there are no 0-th primitive roots of unity.
|