English
The ring of integers $\\mathbb{Z}$ is a Euclidean domain with the standard division algorithm: for all $a,b$ there exist $q,r$ with $a=qb+r$ and $|r|<|b|$. The Euclidean norm is $|\\cdot|$ (via natAbs).
Русский
Множество целых чисел $\\mathbb{Z}$ является евклидовым кольцом с обычной схемой деления: для любых $a,b$ существуют $q,r$ такие, что $a=qb+r$ и $|r|<|b|$. Нормой евклидова алгоритма служит $|\\cdot|$.
LaTeX
$$$\\mathbb{Z}$ is a Euclidean domain with a division algorithm: for all $a,b$ there exist $q,r$ with $a=qb+r$ and $|r|<|b|$.$$
Lean4
instance euclideanDomain : EuclideanDomain ℤ :=
{ inferInstanceAs (CommRing Int),
inferInstanceAs (Nontrivial Int) with
quotient := (· / ·), quotient_zero := Int.ediv_zero, remainder := (· % ·),
quotient_mul_add_remainder_eq := Int.mul_ediv_add_emod, r := fun a b => a.natAbs < b.natAbs,
r_wellFounded := (measure natAbs).wf
remainder_lt := fun a b b0 =>
Int.ofNat_lt.1 <| by
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]
exact Int.emod_lt_abs _ b0
mul_left_not_lt := fun a b b0 =>
not_lt_of_ge <| by
rw [← mul_one a.natAbs, Int.natAbs_mul]
rw [← Int.natAbs_pos] at b0
exact Nat.mul_le_mul_left _ b0 }
