IsCyclotomicExtension.two_pow_norm_zeta_sub_one
theorem IsCyclotomicExtension.two_pow_norm_zeta_sub_one :
∀ {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {k : ℕ},
2 ≤ k →
∀ [inst_3 : IsCyclotomicExtension {2 ^ k} K L],
Irreducible (Polynomial.cyclotomic (2 ^ k) K) →
(Algebra.norm K) (IsCyclotomicExtension.zeta (2 ^ k) K L - 1) = 2
This theorem states that if the cyclotomic polynomial of `2^k` with coefficients in a field `K` (in particular, when `K` is the field of rational numbers) is irreducible and `k` is at least `2`, then the norm of the difference between `zeta (2 ^ k) K L` and 1 in the `K`-algebra is equal to `2`. Here, `zeta (2 ^ k) K L` is a primitive root of unity in the `n`-th cyclotomic extension `L` of `K`, where `n` is `2^k`. The norm is defined as the determinant of the multiplication by the element.
More concisely: If the cyclotomic polynomial of 2^k over field K is irreducible for k ≥ 2, then the norm of zeta(2^k) in the K-algebra of the n-th cyclotomic extension L, where n is 2^k, is equal to 2.
|
IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_sub_one
theorem IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_sub_one :
∀ {p : ℕ+} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {k : ℕ}
[inst_3 : Fact (↑p).Prime] [inst_4 : IsCyclotomicExtension {p ^ (k + 1)} K L],
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) →
p ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L - 1) = ↑↑p
This theorem states that for a given odd prime number `p`, and any natural number `k`, if the `(p ^ (k + 1))`-th cyclotomic polynomial over a field `K` (in particular for `K = ℚ`) is irreducible, then in a cyclotomic extension `L` of `K` of degree `(p ^ (k + 1))`, the norm of the difference between a primitive `(p ^ (k + 1))`-th root of unity in `L` and `1` is equal to `p`.
More concisely: For an odd prime number `p` and natural number `k`, if the `(p ^ (k + 1))`-th cyclotomic polynomial over a field `K` is irreducible, then the norm of the difference between a primitive `(p ^ (k + 1))`-th root of unity in its cyclotomic extension `L` of degree `(p ^ (k + 1))` and 1 equals `p`.
|
IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic
theorem IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic :
∀ {n : ℕ+} {K : Type u} {L : Type v} [inst : Field L] {ζ : L},
IsPrimitiveRoot ζ ↑n →
∀ [inst_1 : Field K] [inst_2 : Algebra K L] [inst_3 : IsCyclotomicExtension {n} K L],
2 < ↑n →
Irreducible (Polynomial.cyclotomic (↑n) K) →
(Algebra.norm K) (ζ - 1) = ↑(Polynomial.eval 1 (Polynomial.cyclotomic ↑n ℤ))
The theorem `IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic` states that for any positive integer `n`, and types `K` and `L` such that `L` is a field, `ζ` is a primitive root of `n` in `L`, `K` is a field, `K` is an algebra over `L`, and `{n}` is a cyclotomic extension of `K` over `L`, if `n` is greater than `2` and the `n`-th cyclotomic polynomial with coefficients in `K` is irreducible, then the norm in the algebra `K` of `ζ - 1` is equal to the integer evaluation at `1` of the `n`-th cyclotomic polynomial with integer coefficients. In particular, this can apply when `K` is the field of rational numbers `ℚ`.
More concisely: For a positive integer `n`, a field `L`, a primitive root `ζ` of `n` in `L`, a field `K` over `L`, and a cyclotomic extension `{n}` of `K` over `L` with irreducible `n`-th cyclotomic polynomial, the norm of `ζ - 1` in `K` equals the integer evaluation of the `n`-th cyclotomic polynomial at `1`.
|
IsCyclotomicExtension.zeta_spec
theorem IsCyclotomicExtension.zeta_spec :
∀ (n : ℕ+) (A : Type w) (B : Type z) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[inst_3 : IsCyclotomicExtension {n} A B], IsPrimitiveRoot (IsCyclotomicExtension.zeta n A B) ↑n
The theorem `IsCyclotomicExtension.zeta_spec` states that for any positive integer `n`, and types `A` and `B` where `A` and `B` are both commutative rings and `B` is an `A`-algebra, given that `B` is an `n`-th cyclotomic extension of `A`, the function `zeta n A B`, as defined in the context of `IsCyclotomicExtension`, is a primitive `n`-th root of unity. This means that the output of the `zeta` function is an element in `B` that generates the cyclic group of `n`-th roots of unity.
More concisely: For any positive integer `n`, if `B` is an `n`-th cyclotomic extension of the commutative ring `A`, then the `zeta_n` function output of `IsCyclotomicExtension` for `A` and `B` is a primitive `n`-th root of unity in `B`.
|
IsPrimitiveRoot.norm_eq_one
theorem IsPrimitiveRoot.norm_eq_one :
∀ {n : ℕ+} {K : Type u} {L : Type v} [inst : CommRing L] {ζ : L},
IsPrimitiveRoot ζ ↑n →
∀ [inst_1 : Field K] [inst_2 : Algebra K L] [inst_3 : IsDomain L] [inst_4 : IsCyclotomicExtension {n} K L],
n ≠ 2 → Irreducible (Polynomial.cyclotomic (↑n) K) → (Algebra.norm K) ζ = 1
This theorem states that, given a positive natural number `n`, types `K` and `L`, with `L` being a commutative ring, and an element `ζ` of `L` that is a primitive root of `n`, if `K` is a field, `L` is an algebra over `K`, `L` is a domain, and `L` is a cyclotomic extension of `K` with `n`, then if `n` is not equal to `2` and the `n`-th cyclotomic polynomial with coefficients in `K` is irreducible (in particular, if `K` is the field of rational numbers), the norm of `ζ` in the algebra `L` over `K` is equal to `1`.
In simpler terms, the theorem says that under certain conditions involving cyclotomic extensions and irreducible cyclotomic polynomials, the norm of a primitive root (other than `2`) in an algebra is always `1`.
More concisely: If `n` is a positive natural number that is not equal to 2, `K` is a field, `L` is a commutative domain that is a cyclotomic extension of `K` with basis `{1, ζ, ζ^2, ..., ζ^(n-1)}` for some primitive root `ζ` of `n` in `L`, and the corresponding `n`-th cyclotomic polynomial is irreducible over `K`, then the norm of `ζ` in `L` over `K` equals 1.
|
IsCyclotomicExtension.prime_ne_two_norm_zeta_sub_one
theorem IsCyclotomicExtension.prime_ne_two_norm_zeta_sub_one :
∀ {p : ℕ+} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : Fact (↑p).Prime] [inst_4 : IsCyclotomicExtension {p} K L],
Irreducible (Polynomial.cyclotomic (↑p) K) →
p ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta p K L - 1) = ↑↑p
This theorem states that if the cyclotomic polynomial of a positive integer `p` over a field `K` is irreducible, and `p` is an odd prime number, then the norm of the difference between a primitive root of unity in a cyclotomic extension `L` of `K` and 1 is `p`. This applies specifically when `K` is the field of rational numbers. In the context of algebra, the norm of an element of an algebra is the determinant of the multiplication by that element, and irreducibility of a polynomial means it cannot be factored into polynomials of lower degree.
More concisely: If `p` is an odd prime number and the cyclotomic polynomial of `p` over the rational numbers is irreducible, then the norm of the difference between a primitive root of unity in the cyclotomic extension and 1 is equal to `p`.
|
IsPrimitiveRoot.pow_sub_one_norm_prime_pow_of_ne_zero
theorem IsPrimitiveRoot.pow_sub_one_norm_prime_pow_of_ne_zero :
∀ {p : ℕ+} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k s : ℕ},
IsPrimitiveRoot ζ ↑(p ^ (k + 1)) →
∀ [hpri : Fact (↑p).Prime] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L],
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) →
s ≤ k → k ≠ 0 → (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
This theorem states that given a prime number `p`, field types `K` and `L`, a root of unity `ζ`, and nonnegative integers `k` and `s`, if `ζ` is a primitive `(p^(k+1))`-th root of unity and the `(p^(k+1))`-th cyclotomic polynomial is irreducible, then as long as `k` is not zero and `s` is less than or equal to `k`, the norm of the expression `(ζ^(p^s) - 1)` over the field `K` will be `p` to the power of `p^s`. The theorem particularly applies when `K` is the field of rational numbers (`ℚ`). IsCyclotomicExtension `{p ^ (k + 1)} K L` ensures that `L` is a cyclotomic extension of `K` generated by the `(p^(k+1))`-th roots of unity.
More concisely: Given a prime number `p`, a root of unity `ζ` of order `p^(k+1)`, and a cyclotomic extension `L` over `K` generated by `ζ`, if the `(p^(k+1))`-th cyclotomic polynomial is irreducible and `k ≠ 0`, then the norm of `(ζ^(p^s) - 1)` over `K` equals `p^(p^s)` for all `0 ≤ s ≤ k`.
|
IsPrimitiveRoot.sub_one_norm_two
theorem IsPrimitiveRoot.sub_one_norm_two :
∀ {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
IsPrimitiveRoot ζ (2 ^ k) →
2 ≤ k →
∀ [H : IsCyclotomicExtension {2 ^ k} K L],
Irreducible (Polynomial.cyclotomic (2 ^ k) K) → (Algebra.norm K) (ζ - 1) = 2
The theorem `IsPrimitiveRoot.sub_one_norm_two` states that if the cyclotomic polynomial of power `2 ^ k` over a field `K` (`ℚ` in particular) is irreducible and `k` is greater than or equal to `2`, then the norm of `ζ - 1` is `2`. Here, `ζ` is a primitive root of order `2 ^ k` and `K` and `L` are fields with algebra structure. It also assumes that the set `{2 ^ k}` forms a cyclotomic extension of the fields `K` and `L`. The norm of an element in an `R`-algebra is the determinant of the multiplication by that element.
More concisely: If `ζ` is a primitive root of order `2^k` in fields `K` and `L` with algebra structure where `2^k` forms a cyclotomic extension and the cyclotomatic polynomial of degree `2^k` over `K` (or `L`) is irreducible, then `∥ζ - 1∥ = 2` where `∥.∥` denotes the norm in the `R`-algebra.
|
IsCyclotomicExtension.norm_zeta_eq_one
theorem IsCyclotomicExtension.norm_zeta_eq_one :
∀ {n : ℕ+} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension {n} K L],
n ≠ 2 → Irreducible (Polynomial.cyclotomic (↑n) K) → (Algebra.norm K) (IsCyclotomicExtension.zeta n K L) = 1
This theorem states that, for any positive natural number `n` that is not equal to 2, and for any types `K` and `L` representing fields in which `K` can be viewed as an algebra over `L`, if `K` is an `n`-th cyclotomic extension of `L` and the `n`-th cyclotomic polynomial with coefficients in `K` is irreducible, then the norm of a primitive `n`-th root of unity in `K` (denoted `zeta n K L`) is `1`. Note that this is particularly applicable when `K` is the field of rational numbers, `ℚ`.
More concisely: For any prime number `n` and fields `K` being an `n`-th cyclotomic extension of `L` with the irreducible `n`-th cyclotomic polynomial over `K`, the norm of a primitive `n`-th root of unity in `K` equals 1.
|
IsPrimitiveRoot.norm_eq_neg_one_pow
theorem IsPrimitiveRoot.norm_eq_neg_one_pow :
∀ {K : Type u} {L : Type v} [inst : CommRing L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
IsPrimitiveRoot ζ 2 → ∀ [inst_3 : IsDomain L], (Algebra.norm K) ζ = (-1) ^ FiniteDimensional.finrank K L
This theorem states that if `ζ` is a primitive root of order 2 in a commutative ring `L`, which is also a field `K`-algebra, then for `L` as a domain, the algebraic norm of `ζ` is equals to `(-1)` raised to the power of the finite rank of the `K`-algebra `L`. In simpler terms, for a specific type of algebraic structure, the determinant of the linear map `(*) ζ` is equal to `(-1)` to the power of the dimension of the space, given that `ζ` is a root of unity of order 2.
More concisely: If `ζ` is a primitive root of order 2 in a finite-dimensional `K`-algebra `L` over a field `K`, then the algebraic norm of `ζ` equals `(-1)` raised to the power of the algebra's dimension as a domain.
|
IsPrimitiveRoot.pow_sub_one_norm_prime_pow_ne_two
theorem IsPrimitiveRoot.pow_sub_one_norm_prime_pow_ne_two :
∀ {p : ℕ+} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k s : ℕ},
IsPrimitiveRoot ζ ↑(p ^ (k + 1)) →
∀ [hpri : Fact (↑p).Prime] [inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L],
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) →
s ≤ k → p ^ (k - s + 1) ≠ 2 → (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
The theorem `IsPrimitiveRoot.pow_sub_one_norm_prime_pow_ne_two` states that if `ζ` is a primitive root of unity of order `p^(k+1)` for some prime `p` and positive integer `k`, and if the `p^(k+1)`-th cyclotomic polynomial is irreducible over a field `K` (which can be the rational numbers `ℚ`), then the norm of `ζ^(p^s) - 1` in the algebra over `K` is `p^(p^s)` provided `s` is less than or equal to `k` and `p^(k-s+1)` is different from `2`. This theorem is significant to number theory and algebra, especially in the study of cyclotomic fields and their norms.
More concisely: If `ζ` is a primitive root of unity of order `p^(k+1)` in a field `K`, and the `p^(k+1)`-th cyclotomic polynomial is irreducible over `K`, then the norm of `ζ^(p^s) - 1` in `K` is `p^(p^s)` for `s` less than or equal to `k` and `p^(k-s+1)` not equal to 2.
|
IsPrimitiveRoot.pow_sub_one_norm_two
theorem IsPrimitiveRoot.pow_sub_one_norm_two :
∀ {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
IsPrimitiveRoot ζ (2 ^ (k + 1)) →
∀ [inst_3 : IsCyclotomicExtension {2 ^ (k + 1)} K L],
Irreducible (Polynomial.cyclotomic (2 ^ (k + 1)) K) → (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
This theorem states that for any field `L` and `K`, with `K` being an algebra over `L`, and any natural number `k`, if `ζ` is a primitive root of `2 ^ (k + 1)`, and if the cyclotomic polynomial of order `2 ^ (k + 1)` with coefficients in `K` is irreducible, then the norm in the algebra `K` of `ζ ^ 2 ^ k - 1` is equal to `(-2) ^ 2 ^ k`. This theorem also holds in particular when the field `K` is the field of rational numbers (`ℚ`).
In simpler terms, this theorem connects some properties of a primitive root of unity, the irreducibility of a certain cyclotomic polynomial and the value of the norm of a specific algebraic expression.
More concisely: For any field `K` being an algebra over a field `L`, and for any natural number `k` such that the cyclotomic polynomial of order `2^(k+1)` over `K` is irreducible and `ζ` is a primitive root of unity of order `2^(k+1)` in `K`, the norm of `ζ^(2^k) - 1` equals `(-2) ^ 2^k`.
|
IsCyclotomicExtension.finrank
theorem IsCyclotomicExtension.finrank :
∀ {n : ℕ+} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : CommRing L] [inst_2 : IsDomain L]
[inst_3 : Algebra K L] [inst_4 : IsCyclotomicExtension {n} K L],
Irreducible (Polynomial.cyclotomic (↑n) K) → FiniteDimensional.finrank K L = (↑n).totient
The theorem `IsCyclotomicExtension.finrank` states that if the `n`-th cyclotomic polynomial is irreducible over a field `K` (for instance, when `K` is the field of rational numbers), then the rank (or dimension) of the field extension generated by a root of this cyclotomic polynomial is equal to the totient function of `n`. In other words, the dimension of the cyclotomic extension is equal to the number of integers less than `n` that are relatively prime to `n`.
More concisely: If the n-th cyclotomic polynomial is irreducible over a field K, then the dimension of the field extension generated by a root of this polynomial is equal to the Euler totient function φ(n).
|
IsPrimitiveRoot.sub_one_norm_isPrimePow
theorem IsPrimitiveRoot.sub_one_norm_isPrimePow :
∀ {n : ℕ+} {K : Type u} {L : Type v} [inst : Field L] {ζ : L},
IsPrimitiveRoot ζ ↑n →
∀ [inst_1 : Field K] [inst_2 : Algebra K L],
IsPrimePow ↑n →
∀ [inst_3 : IsCyclotomicExtension {n} K L],
Irreducible (Polynomial.cyclotomic (↑n) K) → n ≠ 2 → (Algebra.norm K) (ζ - 1) = ↑(↑n).minFac
The theorem states that for a positive natural number `n` which is a prime power (excluding `2`) and a primitive root `ζ` of `n` in a field `L`, if the `n`-th cyclotomic polynomial is irreducible over a field `K` (such as rational numbers `ℚ`), then the norm of `ζ - 1` in an `R`-algebra `K` is equal to the smallest prime factor of `n`. The `n`-th cyclotomic polynomial being irreducible is a condition specifying that it cannot be factored into simpler polynomials over `K`. The norm of an element in an `R`-algebra is the determinant of the multiplication by that element.
More concisely: For a prime power `n` (excluding 2) and its primitive root `ζ` in a field `L`, if the `n`-th cyclotomic polynomial is irreducible over field `K`, then the norm of `ζ - 1` in `K` equals the smallest prime factor of `n`.
|
IsCyclotomicExtension.isPrimePow_norm_zeta_sub_one
theorem IsCyclotomicExtension.isPrimePow_norm_zeta_sub_one :
∀ {n : ℕ+} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
IsPrimePow ↑n →
∀ [inst_3 : IsCyclotomicExtension {n} K L],
Irreducible (Polynomial.cyclotomic (↑n) K) →
n ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta n K L - 1) = ↑(↑n).minFac
The theorem states that if `n` is a positive natural number that is also a prime power (meaning that `n` can be written as a power of a prime number), and `n` is not equal to 2, and the `n`-th cyclotomic polynomial with coefficients in a field `K` is irreducible (in particular, when `K` is the field of rational numbers), then the norm of the difference between a primitive root of unity in a `n`-th cyclotomic extension of `K` and 1 (expressed as `zeta n K L - 1`) equals the smallest prime factor of `n`.
More concisely: If `n` is a positive prime power natural number not equal to 2, and the `n`-th cyclotomic polynomial is irreducible over a field `K`, then the norm of the difference between a primitive root of unity in the `n`-th cyclotomic extension of `K` and 1 equals the smallest prime factor of `n`.
|
IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_pow_sub_one
theorem IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_pow_sub_one :
∀ {p : ℕ+} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {k : ℕ}
[inst_3 : Fact (↑p).Prime] [inst_4 : IsCyclotomicExtension {p ^ (k + 1)} K L],
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) →
∀ {s : ℕ},
s ≤ k →
p ^ (k - s + 1) ≠ 2 →
(Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
This theorem states that for a given prime number `p` and integers `k` and `s` with `s` less than or equal to `k` and `p ^ (k - s + 1)` not equal to 2, if the `p ^ (k + 1)`-th cyclotomic polynomial is irreducible over a field `K` (particularly for `K` equal to the field of rational numbers `ℚ`), then the norm in the `K` algebra of the difference between the power `p ^ s` of a primitive root of unity in an `n`-th cyclotomic extension `L` of `K` and 1 is equal to `p ^ (p ^ s)`. In other words, the norm of `(zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1` is `p ^ (p ^ s)`.
More concisely: If `p` is a prime number, `k` and `s` are integers with `s <= k` and `p ^ (k - s + 1) != 2`, and the `p ^ (k + 1)`-th cyclotomic polynomial is irreducible over a field `K`, then the norm of `(zeta^(p^(k+1)) - 1)` in `K`'s algebraic closure is `p ^ (p ^ s)`.
|
IsPrimitiveRoot.pow_sub_one_norm_prime_ne_two
theorem IsPrimitiveRoot.pow_sub_one_norm_prime_ne_two :
∀ {p : ℕ+} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
IsPrimitiveRoot ζ ↑(p ^ (k + 1)) →
∀ [hpri : Fact (↑p).Prime] [inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L],
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) →
∀ {s : ℕ}, s ≤ k → p ≠ 2 → (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
This theorem states that for a given positive prime number `p`, fields `K` and `L`, an element `ζ` of `L`, and a natural number `k`, if `ζ` is a primitive root of `(p ^ (k + 1))`, `(p ^ (k + 1))` is a cyclotomic extension of `K` over `L`, and the `(p ^ (k + 1))`-th cyclotomic polynomial is irreducible over `K`, then for any natural number `s` less than or equal to `k`, if `p` is not equal to 2, the norm of `ζ ^ (p ^ s) - 1` over `K` is equal to `p ^ (p ^ s)`. In particular, this applies when `K` is the set of rational numbers.
In simpler terms, if we have a certain mathematical structure involving roots of unity, prime numbers, and polynomial irreducibility, then there's a specific relationship between the prime number, the root of unity, and their norm, as long as the prime number isn't 2.
More concisely: If `p` is a positive prime number, `ζ` is a primitive root of `(p ^ (k + 1))` in field `L`, `(p ^ (k + 1))` is a cyclotomic extension of `K` over `L`, and the `(p ^ (k + 1))`-th cyclotomic polynomial is irreducible over `K`, then for any natural number `s` less than or equal to `k`, the norm of `ζ ^ (p ^ s) - 1` over `K` equals `p ^ (p ^ s)`.
|
IsPrimitiveRoot.norm_eq_one_of_linearly_ordered
theorem IsPrimitiveRoot.norm_eq_one_of_linearly_ordered :
∀ {n : ℕ+} {L : Type v} [inst : CommRing L] {ζ : L},
IsPrimitiveRoot ζ ↑n →
∀ {K : Type u_1} [inst_1 : LinearOrderedField K] [inst_2 : Algebra K L], Odd ↑n → (Algebra.norm K) ζ = 1
The theorem `IsPrimitiveRoot.norm_eq_one_of_linearly_ordered` states that for any positive natural number `n`, a type `L` with a commutative ring structure, and an element `ζ` in `L` that is a primitive root of `n`, given that `L` is a `K`-algebra where `K` is a linearly ordered field, if `n` is an odd number then the norm of `ζ` in the `K`-algebra is `1`. In other words, if `ζ` is a primitive nth root of unity in a commutative ring `L`, which is an algebra over a linearly ordered field `K`, and if `n` is odd, then the determinant of the linear transformation given by multiplication by `ζ` is `1` in `K`.
More concisely: If `ζ` is a primitive root of odd order `n` in a commutative `K`-algebra `L`, then the norm of `ζ` is equal to 1 in `K`.
|
IsPrimitiveRoot.sub_one_norm_prime
theorem IsPrimitiveRoot.sub_one_norm_prime :
∀ {p : ℕ+} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L]
[hpri : Fact (↑p).Prime] [hcyc : IsCyclotomicExtension {p} K L],
IsPrimitiveRoot ζ ↑p → Irreducible (Polynomial.cyclotomic (↑p) K) → p ≠ 2 → (Algebra.norm K) (ζ - 1) = ↑↑p
The theorem states that, given a positive integer `p` and two fields `K` and `L` with an algebra structure between them, if `p` is an odd prime number and the `p`-th cyclotomic polynomial over `K` is irreducible (in particular when `K` is the field of rational numbers) and if `ζ` is a primitive `p`-th root of unity in `L`, then the algebraic norm of `(ζ - 1)` over `K` is equal to `p`. The theorem assumes that `L` is a cyclotomic extension of `K` generated by the `p`-th roots of unity.
More concisely: Given an odd prime number `p`, a field `K` with an algebra structure, a cyclotomic extension `L` of `K` generated by primitive `p`-th roots of unity, and a primitive `p`-th root of unity `ζ` in `L`, the norm of `ζ - 1` from `L` to `K` equals `p`.
|
IsPrimitiveRoot.sub_one_norm_prime_ne_two
theorem IsPrimitiveRoot.sub_one_norm_prime_ne_two :
∀ {p : ℕ+} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
IsPrimitiveRoot ζ ↑(p ^ (k + 1)) →
∀ [hpri : Fact (↑p).Prime] [inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L],
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) → p ≠ 2 → (Algebra.norm K) (ζ - 1) = ↑↑p
The theorem `IsPrimitiveRoot.sub_one_norm_prime_ne_two` states that for any positive integer `p`, types `K` and `L`, where `L` is a field, `ζ` is an element of `L`, `K` is a field, `K` is an algebra over `L`, and `k` is a natural number, if `ζ` is a primitive root of `p ^ (k + 1)`, `p` is an odd prime number, the cyclotomic polynomial of `p ^ (k + 1)` with coefficients in `K` is irreducible, and the set `{p ^ (k + 1)}` is a cyclotomic extension of `K` in `L`, then the norm of `ζ - 1` (where "norm" refers to the determinant of `(*) s` in the `R`-algebra `s`) is equivalent to `p`. This theorem effectively links the norm of an element in algebra to the properties of prime numbers and cyclotomic polynomials.
More concisely: If `ζ` is a primitive root of `p^(k+1)`, `p` is an odd prime, the cyclotomic polynomial of `p^(k+1)` over `K` is irreducible, and `{p^(k+1)}` is a cyclotomlic extension of `K` in `L`, then the norm of `ζ-1` in the `R`-algebra `s` equals `p`.
|