isIntegral_rat_I — Mathlib

English

The imaginary unit I is integral over the rationals, since it is integral over the integers and the integers embed in the rationals.

Русский

Мнимая единица I интегральна над полями рациональных чисел, так как она интегральна над Z и Z вложено в Q.

LaTeX

$$$\exists p \in \mathbb{Q}[X],\; p \text{ monic} \land p(I) = 0$$$

Lean4

theorem isIntegral_rat_I : IsIntegral ℚ I :=
  isIntegral_int_I.tower_top

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