div_def — Mathlib

English

Division in Gaussian integers is given by rounding the real and imaginary parts of (x * conjugate(y))/norm(y).

Русский

Деление в ℤ[i] задается округлением действительной и мнимой части дроби (x * conj(y)) / norm(y).

LaTeX

$$$ x / y = \langle \operatorname{round}\left(\dfrac{(x \cdot \overline{y}).\mathrm{re}}{\|y\|^2}, \right) , \operatorname{round}\left(\dfrac{(x \cdot \overline{y}).\mathrm{im}}{\|y\|^2} , \right) \rangle $$$

Lean4

theorem div_def (x y : ℤ[i]) : x / y = ⟨round ((x * star y).re / norm y : ℚ), round ((x * star y).im / norm y : ℚ)⟩ :=
  show Zsqrtd.mk _ _ = _ by simp [div_eq_mul_inv]

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