Polynomial.IsSplittingField.splits
theorem Polynomial.IsSplittingField.splits :
∀ {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : Polynomial K)
[inst_3 : Polynomial.IsSplittingField K L f], Polynomial.Splits (algebraMap K L) f
This theorem states that for any field `K` and any splitting field `L` over `K` for a polynomial `f`, the polynomial `f` splits over `L`. More specifically, the polynomial `f` maps to zero or all of its irreducible factors have degree 1 under the embedding given by the algebra structure from `K` to `L`. The splitting of a polynomial is defined by the condition that every irreducible factor of the polynomial over the field has degree 1. The concept of a splitting field concerns the field extension in which a given polynomial can be factored into linear factors.
More concisely: For any field `K`, polynomial `f` over `K`, and splitting field `L` of `f` over `K`, `f`splits into linear factors in `L`.
|
Polynomial.IsSplittingField.adjoin_rootSet
theorem Polynomial.IsSplittingField.adjoin_rootSet :
∀ {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : Polynomial K)
[inst_3 : Polynomial.IsSplittingField K L f], Algebra.adjoin K (f.rootSet L) = ⊤
This theorem states that for any fields `K` and `L` with an algebra structure over `K` and `L`, and given a polynomial `f` over `K` for which `L` is a splitting field, the subalgebra generated by adjoining the set of distinct roots of `f` in `L` to `K` is in fact the whole of `L`. In other words, the field `L` is generated by the roots of the polynomial `f` over `K`.
More concisely: If `K` is a field, `L` is a field with an algebra structure over `K`, and `f` is a polynomial over `K` such that `L` is a splitting field for `f` over `K`, then the subalgebra of `L` generated by the roots of `f` is equal to `L`.
|
Polynomial.IsSplittingField.finiteDimensional
theorem Polynomial.IsSplittingField.finiteDimensional :
∀ {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : Polynomial K)
[inst_3 : Polynomial.IsSplittingField K L f], FiniteDimensional K L
This theorem states that for any field `K` and `L`, where `K` is an algebra over `L`, if a polynomial `f` defined over field `K` is a splitting field over `L`, then `L` is a finite dimensional vector space over `K`. Here, a polynomial is said to be a splitting field if it splits into linear factors (roots) in the field. The notion of finite dimensionality for a vector space implies that the vector space can be spanned by a finite set of vectors.
More concisely: If a polynomial `f` over field `K` is a splitting field for `K` over `L`, then `L` is a finite-dimensional vector space over `K`.
|