isGalois_iff — Mathlib

English

An extension IsGalois F E is equivalent to the conjunction of Algebra.IsSeparable F E and Normal F E; i.e., IsGalois F E iff the extension is separable and normal.

Русский

Расширение IsGalois F E эквивалентно сочетанию разделимости и нормальности: IsGalois F E ⇔ Algebra.IsSeparable F E ∧ Normal F E.

LaTeX

$$$IsGalois F E \\iff (Algebra.IsSeparable F E \\land Normal F E)$$$

Lean4

theorem isGalois_iff : IsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E :=
  ⟨fun h => ⟨h.1, h.2⟩, fun h =>
    { to_isSeparable := h.1
      to_normal := h.2 }⟩

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