normal_iff — Mathlib

English

Normal F K is equivalent to: for every x ∈ K, x is integral over F and minpoly splits over K.

Русский

Нормальность F над K эквивалентна тому, что для каждого x ∈ K x интегрально над F и minpoly(x) раскладывается в K.

LaTeX

$$$\mathrm{Normal} F K \iff \forall x \in K, (\IsIntegral F x) \land \mathrm{Splits} (\mathrm{algebraMap} F K) (\minpoly F x)$$$

Lean4

theorem normal_iff : Normal F K ↔ ∀ x : K, IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x) :=
  ⟨fun h x => ⟨h.isIntegral x, h.splits x⟩, fun h =>
    { isAlgebraic := fun x => (h x).1.isAlgebraic
      splits' := fun x => (h x).2 }⟩

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