mathlib3 documentation


Splitting fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file introduces the notion of a splitting field of a polynomial and provides an embedding from a splitting field to any field that splits the polynomial. A polynomial f : K[X] splits over a field extension L of K if it is zero or all of its irreducible factors over L have degree 1. A field extension of K of a polynomial f : K[X] is called a splitting field if it is the smallest field extension of K such that f splits.

Main definitions #

Main statements #

@[protected, instance]
theorem polynomial.is_splitting_field.mul {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [algebra K L] [algebra F K] [algebra F L] [is_scalar_tower F K L] (f g : polynomial F) (hf : f 0) (hg : g 0) [polynomial.is_splitting_field F K f] [polynomial.is_splitting_field K L ( (algebra_map F K) g)] :
noncomputable def polynomial.is_splitting_field.lift {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [algebra K L] [algebra K F] (f : polynomial K) [polynomial.is_splitting_field K L f] (hf : polynomial.splits (algebra_map K F) f) :

Splitting field of f embeds into any field that splits f.

theorem intermediate_field.splits_of_splits {K : Type v} {L : Type w} [field K] [field L] [algebra K L] {p : polynomial K} {F : intermediate_field K L} (h : polynomial.splits (algebra_map K L) p) (hF : (x : L), x p.root_set L x F) :