separable — Mathlib

English

If R ⊆ K is such that every monic irreducible polynomial over R splits over K, then IsAlgClosure R K.

Русский

Если каждый монический ирредуцируемый полином над R распадается над K, тогда IsAlgClosure R K.

LaTeX

$$$\forall p : R[X], p.Monic \rightarrow Irreducible p \rightarrow Polynomial.Splits (algebraMap R K) p \rightarrow IsAlgClosure R K$$$

Lean4

instance (priority := 100) separable (R K : Type*) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] [CharZero R] :
    Algebra.IsSeparable R K :=
  ⟨fun _ => (minpoly.irreducible (Algebra.IsIntegral.isIntegral _)).separable⟩

Похожие утверждения