Field.exists_primitive_element_of_finite_bot
theorem Field.exists_primitive_element_of_finite_bot :
∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : Finite F]
[inst_4 : FiniteDimensional F E], ∃ α, F⟮α⟯ = ⊤
The theorem `Field.exists_primitive_element_of_finite_bot` states that for any given finite field `F` and any finite dimensional extension `E` of this field, there exists an element `α` such that the field generated by `F` and `α` is the whole field `E`. This is essentially the Primitive Element Theorem but specifically for a finite dimensional extension of a finite field. The Primitive Element Theorem is a fundamental result in field theory, and in this particular case, it guarantees the existence of a "primitive element" that generates the entire field extension when adjoined to the base field.
More concisely: For any finite field `F` and finite dimensional extension `E` of `F`, there exists an element `α` in `E` such that `F(α) = E`.
|
Field.exists_primitive_element_of_finite_top
theorem Field.exists_primitive_element_of_finite_top :
∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : Finite E],
∃ α, F⟮α⟯ = ⊤
This is the **Primitive Element Theorem** for finite fields. Given any two types `F` and `E` where `F` and `E` are fields, and `E` is a finite field extension of `F`, the theorem asserts that there exists an element `α` in `E` such that the subfield of `E` generated by `F` and `α` equals `E`. In other words, every finite field extension is generated by one element.
More concisely: Every finite field extension has a primitive element, that is, an element whose presence in the extension generates the entire field.
|
Field.exists_primitive_element_iff_finite_intermediateField
theorem Field.exists_primitive_element_iff_finite_intermediateField :
∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
(Algebra.IsAlgebraic F E ∧ ∃ α, F⟮α⟯ = ⊤) ↔ Finite (IntermediateField F E)
The Steinitz Theorem states that for an algebraic extension `E` of a field `F`, there exists a primitive element (meaning, there exists an element `α` in `E` such that the subalgebra generated by `F` and `α` equals the top subalgebra of `F` in `E`) if and only if there are only a finite number of intermediate fields between `E` and `F`. In this context, an intermediate field is a field that contains `F` and is contained in `E`.
More concisely: The Steinitz Theorem asserts that an algebraic extension of a field has a primitive element if and only if the number of intermediate fields between the extension and the base field is finite.
|
Field.exists_primitive_element
theorem Field.exists_primitive_element :
∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : FiniteDimensional F E] [inst_4 : IsSeparable F E], ∃ α, F⟮α⟯ = ⊤
This is the **Primitive Element Theorem**. It states that for any finite separable field extension `E` over `F`, there exists a primitive element. In other words, there exists an element `α` in `E` such that the field generated by `F` and `α` equals the whole field `E`. This theorem is a fundamental result in field theory and it essentially says that any finite separable field extension is generated by a single element.
More concisely: Any finite separable field extension has a primitive element, that is, there exists an element generating the entire extension.
|
Field.primitive_element_inf_aux
theorem Field.primitive_element_inf_aux :
∀ (F : Type u_1) [inst : Field F] [inst_1 : Infinite F] {E : Type u_2} [inst_2 : Field E] (α β : E)
[inst_3 : Algebra F E] [inst_4 : IsSeparable F E], ∃ γ, F⟮α, β⟯ = F⟮γ⟯
This theorem is a vital part of the proof of the Primitive Element Theorem. It states that for any infinite field `F` and any two separable elements `α` and `β` over `F`, the field generated by `α` and `β` can be generated by just one element `γ`. In other words, it is possible to find such a `γ` that `F⟮α, β⟯` is equivalent to `F⟮γ⟯`.
More concisely: For any infinite separably extended field `F`, and two separable elements `α` and `β` in `F`, there exists an element `γ` such that `F(α, β) = F(γ)`.
|