instDiv — Mathlib

English

For all x,y ∈ ℤ[i], the squared norm of the difference between x/y (as a complex number) and its Gaussian-integer quotient is less than 1: Complex.normSq((x/y) - ((x/y) : ℤ[i]) : ℂ) < 1.

Русский

Для любых x,y ∈ ℤ[i] квадрат нормы разности между x/y как комплекс и его частным по гауссовым целым меньше 1: Complex.normSq((x/y) − (x/y) какGaussianInt).

LaTeX

$$$ \operatorname{normSq}\Bigl((x / y : \mathbb{Z}[i]) : \mathbb{C} \; - \; (x / y : \mathbb{C})\Bigr) < 1 $$$

Lean4

instance : Div ℤ[i] :=
  ⟨fun x y =>
    let n := (norm y : ℚ)⁻¹
    let c := star y
    ⟨round ((x * c).re * n : ℚ), round ((x * c).im * n : ℚ)⟩⟩

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