exists_root_adjoin_eq_top_of_isCyclic
theorem exists_root_adjoin_eq_top_of_isCyclic :
∀ (K : Type u) [inst : Field K] (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : IsGalois K L]
[inst_4 : FiniteDimensional K L] [inst_5 : IsCyclic (L ≃ₐ[K] L)],
(primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty →
∃ α, α ^ FiniteDimensional.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
The theorem `exists_root_adjoin_eq_top_of_isCyclic` states that if `L/K` is a cyclic field extension with degree `n`, and the field `K` contains all `n`-th roots of unity, then the field `L` can be obtained by adjoining a single element `α` to `K`, where `α` to the power `n` lies in `K`. In mathematical notation, this is expressed as `L = K(α)` where `α^n ∈ K`. This theorem underscores the idea that a cyclic extension can be generated by a single element whose `n`-th power lies in the base field, provided all `n`-th roots of unity belong to the base field.
More concisely: If `L/K` is a cyclic field extension of degree `n` with `K` containing all `n`-th roots of unity, then `L = K(α)` for some `α ∈ L` such that `α^n ∈ K`.
|
Polynomial.separable_X_pow_sub_C_of_irreducible
theorem Polynomial.separable_X_pow_sub_C_of_irreducible :
∀ {K : Type u} [inst : Field K] {n : ℕ},
(primitiveRoots n K).Nonempty →
∀ (a : K), Irreducible (Polynomial.X ^ n - Polynomial.C a) → (Polynomial.X ^ n - Polynomial.C a).Separable
The theorem `Polynomial.separable_X_pow_sub_C_of_irreducible` states that for any type `K` with a field structure and a natural number `n`, if the set of `n`-th primitive roots of unity in `K` is non-empty, then for any element `a` in `K`, if the polynomial `X^n - a` is irreducible, it is also separable. In other words, if you have a polynomial of the form `X^n - a` that cannot be factored into simpler polynomials in a field where there exists an `n`-th primitive root of unity, then that polynomial does not have any multiple roots.
More concisely: If `K` is a field with a non-empty set of `n`-th primitive roots of unity, and `X^n - a` is an irreducible polynomial in `K[X]`, then `X^n - a` is separable.
|
ne_zero_of_irreducible_X_pow_sub_C
theorem ne_zero_of_irreducible_X_pow_sub_C :
∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K}, Irreducible (Polynomial.X ^ n - Polynomial.C a) → n ≠ 0
The theorem `ne_zero_of_irreducible_X_pow_sub_C` states that for any field `K`, any natural number `n`, and any element `a` of `K`, if the polynomial `X^n - C a` is irreducible, then `n` is not equal to zero. Here, `X` denotes the polynomial variable and `C a` represents a constant polynomial with coefficient `a`. Irreducible, in the context of polynomials, means the polynomial cannot be factored into two non-trivial polynomials.
More concisely: If `X^n - Ca` is an irreducible polynomial over a field `K`, then `n` is different from zero.
|
isCyclic_tfae
theorem isCyclic_tfae :
∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : FiniteDimensional K L],
(primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty →
[IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L),
∃ a,
Irreducible (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a) ∧
Polynomial.IsSplittingField K L (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a),
∃ α, α ^ FiniteDimensional.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE
This theorem states that for a given finite extension `L/K` of dimension `n`, where `K` contains all `n`-th roots of unity, the following are equivalent:
1. The extension `L/K` is Galois and cyclic.
2. There exists some element `a` in `K` such that `L` is a splitting field of an irreducible polynomial of the form `X^n - a` in `K[X]`.
3. There exists some `α` in `L` such that `α^n` is in the image of the algebra map from `K` to `L`, and the field generated by `K` and `α` is the entire field `L`.
In simpler terms, the conditions essentially state that the extension is cyclic if and only if `L` splits a certain kind of polynomial from `K`, if and only if `L` is generated by an element whose `n`-th power is in `K`.
More concisely: A finite extension L/K of degree n with K containing all n-th roots of unity is Galois and cyclic if and only if there exists an element a in K such that L is the splitting field of X^n - a in K[X] or equivalently, there exists an element α in L such that α^n is in the image of the algebra map from K to L and L is the field generated by K and α.
|
pow_ne_of_irreducible_X_pow_sub_C
theorem pow_ne_of_irreducible_X_pow_sub_C :
∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K},
Irreducible (Polynomial.X ^ n - Polynomial.C a) → ∀ {m : ℕ}, m ∣ n → m ≠ 1 → ∀ (b : K), b ^ m ≠ a
This theorem states that for any field `K` and any natural numbers `n` and `m`, and any elements `a` and `b` of the field `K`, if the polynomial `X^n - a` is irreducible, and if `m` divides `n` but `m` is not equal to 1, then `b^m` is not equal to `a`. In other words, no non-trivial root of the irreducible polynomial `X^n - a` raises to the power `m` equals to the constant `a`.
More concisely: If `n` divides the degree of an irreducible polynomial `X^n - a` over a field `K`, and `m` is a positive integer divisor of `n` with `m ≠ 1`, then `a ≠ b^m` for any element `b` in `K`.
|
X_pow_sub_C_irreducible_of_odd
theorem X_pow_sub_C_irreducible_of_odd :
∀ {K : Type u} [inst : Field K] {n : ℕ},
Odd n →
∀ {a : K},
(∀ (p : ℕ), p.Prime → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (Polynomial.X ^ n - Polynomial.C a)
The theorem `X_pow_sub_C_irreducible_of_odd` states that for any field `K` and any odd natural number `n`, if for any prime number `p` that divides `n` and any element `b` of `K`, `b` to the power of `p` is not equal to `a`, then the polynomial `X^n - C(a)` is irreducible. In simpler terms, if a polynomial is of the form `X^n - a` where `n` is an odd number and `a` is any constant, and there are no elements in the field which to some prime power that divides `n` equals `a`, then this polynomial cannot be factored into simpler polynomials.
More concisely: For any odd natural number `n` and constant `a` in a field `K` such that for all prime `p` dividing `n` and all `b` in `K`, `b^p ≠ a`, the polynomial `X^n - a` is irreducible.
|