isIntegral_int_I — Mathlib

English

The imaginary unit I is integral over the integers; equivalently, I is a root of a monic polynomial with integer coefficients, namely X^2 + 1.

Русский

Мнимая единица I интегральна над числами целого кольца, то есть является корнем мономного полинома с целыми коэффициентами, например X^2 + 1.

LaTeX

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

Lean4

theorem isIntegral_int_I : IsIntegral ℤ I :=
  by
  refine ⟨X ^ 2 + C 1, monic_X_pow_add_C _ two_ne_zero, ?_⟩
  rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]

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