toComplex_re_div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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