toComplex_im_div — Mathlib

English

The imaginary part of x/y as a Gaussian integer matches the rounding of the imaginary part of x/y in ℂ.

Русский

Мнимая часть x/y как гауссового целого совпадает с округлением мнимой части x/y в ℂ.

LaTeX

$$$ \operatorname{Im}\left(\bigl(x / y : \mathbb{Z}[i]\bigr) \right) = \operatorname{round}\left( x / y : \mathbb{C} \right).\mathrm{im} $$$

Lean4

theorem toComplex_im_div (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).im = round (x / y : ℂ).im :=
  by
  rw [div_def, ← @Rat.round_cast ℝ _ _, ← @Rat.round_cast ℝ _ _]
  simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, add_mul]

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