mathlib documentation

field_theory.splitting_field

def polynomial.splits {α : Type u} {β : Type v} [field α] [field β] :
→+* β)polynomial α → Prop

a polynomial splits iff it is zero or all of its irreducible factors have degree 1

Equations
@[simp]
theorem polynomial.splits_zero {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) :

@[simp]
theorem polynomial.splits_C {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) (a : α) :

theorem polynomial.splits_of_degree_eq_one {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

theorem polynomial.splits_of_degree_le_one {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

theorem polynomial.splits_mul {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} :

theorem polynomial.splits_of_splits_mul {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} :

theorem polynomial.splits_of_splits_of_dvd {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} :
f 0polynomial.splits i fg fpolynomial.splits i g

theorem polynomial.splits_of_splits_gcd_left {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} :

theorem polynomial.splits_of_splits_gcd_right {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} :

theorem polynomial.splits_map_iff {α : Type u} {β : Type v} {γ : Type w} [field α] [field β] [field γ] (i : α →+* β) (j : β →+* γ) {f : polynomial α} :

theorem polynomial.splits_one {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) :

theorem polynomial.splits_of_is_unit {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {u : polynomial α} :

theorem polynomial.splits_X_sub_C {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {x : α} :

theorem polynomial.splits_id_iff_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

theorem polynomial.splits_mul_iff {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} :

theorem polynomial.splits_prod {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {ι : Type w} {s : ι → polynomial α} {t : finset ι} :
(∀ (j : ι), j tpolynomial.splits i (s j))polynomial.splits i (∏ (x : ι) in t, s x)

theorem polynomial.splits_prod_iff {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {ι : Type w} {s : ι → polynomial α} {t : finset ι} :
(∀ (j : ι), j ts j 0)(polynomial.splits i (∏ (x : ι) in t, s x) ∀ (j : ι), j tpolynomial.splits i (s j))

theorem polynomial.exists_root_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :
polynomial.splits i ff.degree 0(∃ (x : β), polynomial.eval₂ i x f = 0)

theorem polynomial.exists_multiset_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

def polynomial.root_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :
polynomial.splits i ff.degree 0 → β

Pick a root of a polynomial that splits.

Equations
theorem polynomial.map_root_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (hf : polynomial.splits i f) (hfd : f.degree 0) :

theorem polynomial.roots_map {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

theorem polynomial.eq_prod_roots_of_splits {α : Type u} {β : Type v} [field α] [field β] {p : polynomial α} {i : α →+* β} :

theorem polynomial.eq_X_sub_C_of_splits_of_single_root {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {x : α} {h : polynomial α} :

theorem polynomial.nat_degree_eq_card_roots {α : Type u} {β : Type v} [field α] [field β] {p : polynomial α} {i : α →+* β} :

theorem polynomial.degree_eq_card_roots {α : Type u} {β : Type v} [field α] [field β] {p : polynomial α} {i : α →+* β} :

theorem polynomial.splits_of_exists_multiset {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} {s : multiset β} :

theorem polynomial.splits_of_splits_id {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

theorem polynomial.splits_iff_exists_multiset {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

theorem polynomial.splits_comp_of_splits {α : Type u} {β : Type v} {γ : Type w} [field α] [field β] [field γ] (i : α →+* β) (j : β →+* γ) {f : polynomial α} :

A monic polynomial p that has as much roots as its degree can be written p = ∏(X - a), for a in p.roots.

A polynomial p that has as much roots as its degree can be written p = p.leading_coeff * ∏(X - a), for a in p.roots.

theorem polynomial.splits_iff_card_roots {α : Type u} [field α] {p : polynomial α} :

A polynomial splits if and only if it has as much roots as its degree.

If p is the minimal polynomial of a over F then F[a] ≃ₐ[F] F[x]/(p)

Equations
theorem lift_of_splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [field F] [field K] [field L] [algebra F K] [algebra F L] (s : finset K) :
(∀ (x : K), x s(∃ (H : is_integral F x), polynomial.splits (algebra_map F L) (minimal_polynomial H)))nonempty ((algebra.adjoin F s) →ₐ[F] L)

If K and L are field extensions of F and we have s : finset K such that the minimal polynomial of each x ∈ s splits in L then algebra.adjoin F s embeds in L.

def polynomial.factor {α : Type u} [field α] :

Non-computably choose an irreducible factor from a polynomial.

Equations
@[instance]
def polynomial.irreducible_factor {α : Type u} [field α] (f : polynomial α) :

theorem polynomial.factor_dvd_of_not_is_unit {α : Type u} [field α] {f : polynomial α} :
¬is_unit ff.factor f

theorem polynomial.factor_dvd_of_degree_ne_zero {α : Type u} [field α] {f : polynomial α} :
f.degree 0f.factor f

theorem polynomial.factor_dvd_of_nat_degree_ne_zero {α : Type u} [field α] {f : polynomial α} :
f.nat_degree 0f.factor f

def polynomial.remove_factor {α : Type u} [field α] (f : polynomial α) :

Divide a polynomial f by X - C r where r is a root of f in a bigger field extension.

Equations
theorem polynomial.nat_degree_remove_factor' {α : Type u} [field α] {f : polynomial α} {n : } :

def polynomial.splitting_field_aux (n : ) {α : Type u} [field α] (f : polynomial α) :
f.nat_degree = nType u

Auxiliary construction to a splitting field of a polynomial. Uses induction on the degree.

Equations
@[instance]
def polynomial.splitting_field_aux.field (n : ) {α : Type u} [field α] {f : polynomial α} (hfn : f.nat_degree = n) :

Equations
@[instance]
def polynomial.splitting_field_aux.inhabited {α : Type u} [field α] {n : } {f : polynomial α} (hfn : f.nat_degree = n) :

Equations
@[instance]
def polynomial.splitting_field_aux.algebra (n : ) {α : Type u} [field α] {f : polynomial α} (hfn : f.nat_degree = n) :

Equations
@[instance]

theorem polynomial.splitting_field_aux.exists_lift (n : ) {α : Type u} [field α] (f : polynomial α) (hfn : f.nat_degree = n) {β : Type u_1} [field β] (j : α →+* β) :

def polynomial.splitting_field {α : Type u} [field α] :
polynomial αType u

A splitting field of a polynomial.

Equations
def polynomial.splitting_field.lift {α : Type u} {β : Type v} [field α] [field β] (f : polynomial α) [algebra α β] :

Embeds the splitting field into any other field that splits the polynomial.

Equations
@[class]
structure polynomial.is_splitting_field (α : Type u) (β : Type v) [field α] [field β] [algebra α β] :
polynomial α → Prop

Typeclass characterising splitting fields.

Instances
@[instance]
def polynomial.is_splitting_field.map {α : Type u} {β : Type v} {γ : Type w} [field α] [field β] [field γ] [algebra α β] [algebra β γ] [algebra α γ] [is_scalar_tower α β γ] (f : polynomial α) [polynomial.is_splitting_field α γ f] :

theorem polynomial.is_splitting_field.splits_iff {α : Type u} (β : Type v) [field α] [field β] [algebra α β] (f : polynomial α) [polynomial.is_splitting_field α β f] :

theorem polynomial.is_splitting_field.mul {α : Type u} (β : Type v) {γ : Type w} [field α] [field β] [field γ] [algebra α β] [algebra β γ] [algebra α γ] [is_scalar_tower α β γ] (f g : polynomial α) (hf : f 0) (hg : g 0) [polynomial.is_splitting_field α β f] [polynomial.is_splitting_field β γ (polynomial.map (algebra_map α β) g)] :

def polynomial.is_splitting_field.lift {α : Type u} (β : Type v) {γ : Type w} [field α] [field β] [field γ] [algebra α β] [algebra α γ] (f : polynomial α) [polynomial.is_splitting_field α β f] :
polynomial.splits (algebra_map α γ) f→ₐ[α] γ)

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

Equations
theorem polynomial.is_splitting_field.finite_dimensional {α : Type u} (β : Type v) [field α] [field β] [algebra α β] (f : polynomial α) [polynomial.is_splitting_field α β f] :

def polynomial.is_splitting_field.alg_equiv {α : Type u} (β : Type v) [field α] [field β] [algebra α β] (f : polynomial α) [polynomial.is_splitting_field α β f] :

Any splitting field is isomorphic to splitting_field f.

Equations