instUniqueEmbOfIsPurelyInseparable

English

If E/F is purely inseparable, then Field.Emb F E has exactly one element.

Русский

Если E/F чисто бесприводно, то полеобразование Field.Emb F E содержит ровно один элемент.

LaTeX

$$$\text{Unique}(\mathrm{Emb} F E)$$$

Lean4

/-- If `E / F` is purely inseparable, then `Field.Emb F E` has exactly one element. -/
instance instUniqueEmbOfIsPurelyInseparable [IsPurelyInseparable F E] : Unique (Emb F E) :=
  instUniqueAlgHomOfIsPurelyInseparable F E _

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