Theorems · Theorem · field theory

IsSepClosed.splits_codomain

∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [IsSepClosed K] {f : k →+* K} (p : Polynomial k),
  p.Separable → (Polynomial.map f p).Splits

Every separable polynomial splits in the field extension f : k →+* K if K is separably closed. See also IsSepClosed.splits_domain for the case where k is separably closed.

Defined in

Mathlib.FieldTheory.IsSepClosed

Cited by

1 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldIsSepClosed