isPurelyInseparable_of_isSepClosed

English

If E over F is an algebraic extension and F is separably closed, then E/F is purely inseparable.

Русский

Если расширение E/F является алгебраическим, и основание F является сепарируемо замкнутым, то E/F чисто безразделимо.

LaTeX

$$$ \text{If } E/F \text{ is algebraic and } IsSepClosed(F)\text{, then } IsPurelyInseparable(F,E). $$$

Lean4

/-- If `E / F` is an algebraic extension, `F` is separably closed,
then `E / F` is purely inseparable. -/
instance isPurelyInseparable_of_isSepClosed {F : Type u} {E : Type v} [Field F] [Ring E] [IsDomain E] [Algebra F E]
    [Algebra.IsAlgebraic F E] [IsSepClosed F] : IsPurelyInseparable F E :=
  ⟨inferInstance, fun x h ↦
    minpoly.mem_range_of_degree_eq_one F x <|
      IsSepClosed.degree_eq_one_of_irreducible F (minpoly.irreducible (Algebra.IsIntegral.isIntegral _)) h⟩

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