isAlgebraic_iff_isIntegral — Mathlib

English

An element of an algebra over a field is algebraic over the base field iff it is integral over the base field.

Русский

Элемент алгебры над полем алгебраичен над базовым полемiff он интегральный над базовым полем.

LaTeX

$$$IsAlgebraic\\; K\\; x \\iff IsIntegral\\; K\\; x$$$

Lean4

/-- An element of an algebra over a field is algebraic if and only if it is integral. -/
theorem isAlgebraic_iff_isIntegral {x : A} : IsAlgebraic K x ↔ IsIntegral K x :=
  by
  refine ⟨?_, IsIntegral.isAlgebraic⟩
  rintro ⟨p, hp, hpx⟩
  refine ⟨_, monic_mul_leadingCoeff_inv hp, ?_⟩
  rw [← aeval_def, map_mul, hpx, zero_mul]

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