inseparable — Mathlib

English

If x ∈ E is separable over F, then x lies in the image of F under the embedding into E.

Русский

Если элемент x над F разделяем над F, то он лежит в образе отображения F в E.

LaTeX

$$$\forall x\in E,\ IsSeparable F x \to x\in (\mathrm{algebraMap} F E).range$$$

Lean4

theorem inseparable [IsPurelyInseparable F E] : ∀ x : E, IsSeparable F x → x ∈ (algebraMap F E).range :=
  IsPurelyInseparable.inseparable'

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