Polynomial.SplittingField.splits
theorem Polynomial.SplittingField.splits :
∀ {K : Type v} [inst : Field K] (f : Polynomial K), Polynomial.Splits (algebraMap K f.SplittingField) f
This theorem asserts that for any field `K` and for any polynomial `f` over `K`, the polynomial `f` splits over its splitting field. In other words, the polynomial `f` can be factored into linear polynomials in the splitting field of `f`. The splitting field of a polynomial is a field extension that contains all the roots of the polynomial. Specifically, the polynomial `f` splits means that it can be expressed as a product of irreducible factors in the splitting field, and since we are in a field, these irreducible factors are linear. The `algebraMap K (Polynomial.SplittingField f)` is a function mapping elements of `K` to their corresponding elements in the splitting field of `f`.
More concisely: For any polynomial `f` over a field `K`, `f` splits in its splitting field, i.e., it can be expressed as a product of linear polynomials in the splitting field.
|
Polynomial.fact_irreducible_factor
theorem Polynomial.fact_irreducible_factor :
∀ {K : Type v} [inst : Field K] (f : Polynomial K), Fact (Irreducible f.factor)
This theorem states that for any field `K` and any polynomial `f` over `K`, the factor of `f` is irreducible. In the context of polynomials, a factor is irreducible if it cannot be factored into a product of two non-constant polynomials, similar to the notion of prime numbers in integer arithmetic. This property is always true and is denoted by the Lean `Fact` wrapper in the conclusion of the theorem.
More concisely: For any field `K` and polynomial `f` over `K`, `f` is irreducible.
|