natAbs_norm_mod_lt

Mathlib.NumberTheory.Zsqrtd.GaussianInt

URI: https://scilib.ai/kg/mathlib#GaussianInt.natAbs_norm_mod_lt

English

For x ∈ ℤ[i] and y ≠ 0, the natural-abs value of the remainder’s norm is less than the natural-abs value of the divisor’s norm.

Русский

Для x ∈ ℤ[i] и y ≠ 0, natAbs(norm(x % y)) < natAbs(norm(y)).

LaTeX

$$$ (x % y).norm.natAbs < y.norm.natAbs $$$

Lean4

theorem natAbs_norm_mod_lt (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs :=
  Int.ofNat_lt.1 <| by simp [norm_mod_lt x hy]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru