Theorems · Theorem · field theory

IsSepClosed.splits_domain

∀ {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_codomain for the case where k is separably closed.

Defined in

Mathlib.FieldTheory.IsSepClosed

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldIsSepClosed