English
The integers admit a normalization monoid structure in which the norm unit of a is 1 if a is nonnegative and -1 otherwise; this unit is compatible with multiplication and with units.
Русский
Целые числа обладают структурой нормализационного моноида, для которой нормализационная единица элемента a равна 1 при a ≥ 0 и −1 иным образом; эта единица совместима с умножением и с единицами обращения.
LaTeX
$$$\operatorname{normUnit}(z) = \begin{cases}1, & z \ge 0 \\ -1, & z < 0\end{cases}$$$
Lean4
instance normalizationMonoid : NormalizationMonoid ℤ
where
normUnit a := if 0 ≤ a then 1 else -1
normUnit_zero := if_pos le_rfl
normUnit_mul {a b} hna
hnb := by
rcases hna.lt_or_gt with ha | ha <;> rcases hnb.lt_or_gt with hb | hb <;>
simp [Int.mul_nonneg_iff, ha.le, ha.not_ge, hb.le, hb.not_ge]
normUnit_coe_units
u :=
(units_eq_one_or u).elim (fun eq => eq.symm ▸ if_pos Int.one_nonneg) fun eq =>
eq.symm ▸ if_neg (not_le_of_gt <| show (-1 : ℤ) < 0 by decide)
