# mathlib3documentation

field_theory.splitting_field.is_splitting_field

# 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 #

• polynomial.is_splitting_field: A predicate on a field to be a splitting field of a polynomial f.

## Main statements #

• polynomial.is_splitting_field.lift: An embedding of a splitting field of the polynomial f into another field such that f splits.
@[class]
structure polynomial.is_splitting_field (K : Type v) (L : Type w) [field K] [field L] [ L] (f : polynomial K) :
Prop

Typeclass characterising splitting fields.

Instances of this typeclass
@[protected, instance]
def polynomial.is_splitting_field.map {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] [ L] [ K] [ L] [ L] (f : polynomial F)  :
theorem polynomial.is_splitting_field.splits_iff {K : Type v} (L : Type w) [field K] [field L] [ L] (f : polynomial K)  :
theorem polynomial.is_splitting_field.mul {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [ L] [ K] [ L] [ L] (f g : polynomial F) (hf : f 0) (hg : g 0) [ (polynomial.map K) g)] :
(f * g)
noncomputable def polynomial.is_splitting_field.lift {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [ L] [ F] (f : polynomial K) (hf : f) :

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

Equations
theorem polynomial.is_splitting_field.finite_dimensional {K : Type v} (L : Type w) [field K] [field L] [ L] (f : polynomial K)  :
theorem polynomial.is_splitting_field.of_alg_equiv {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [ L] [ F] (p : polynomial K) (f : F ≃ₐ[K] L)  :
theorem intermediate_field.splits_of_splits {K : Type v} {L : Type w} [field K] [field L] [ L] {p : polynomial K} {F : L} (h : p) (hF : (x : L), x p.root_set L x F) :
p