surjective_algebraMap_of_isSeparable

English

If E/F is purely inseparable and separable, then the algebra map algebraMap F E is surjective.

Русский

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

LaTeX

$$$ [IsPurelyInseparable(F,E)]\ [Algebra.IsSeparable(F,E)] \, \Rightarrow \, \text{Surjective}(\text{algebraMap } F E). $$$

Lean4

/-- If `E / F` is both purely inseparable and separable, then `algebraMap F E` is surjective. -/
theorem surjective_algebraMap_of_isSeparable [IsPurelyInseparable F E] [Algebra.IsSeparable F E] :
    Function.Surjective (algebraMap F E) := fun x ↦
  IsPurelyInseparable.inseparable F x (Algebra.IsSeparable.isSeparable F x)

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