English
The integers form an additive commutative group.
Русский
Целые числа образуют аддитивную коммутативную группу.
LaTeX
$$$\text{AddCommGroup}(\mathbb{Z}, +)$$$
Lean4
instance instAddCommGroup : AddCommGroup ℤ where
add_comm := Int.add_comm
add_assoc := Int.add_assoc
add_zero := Int.add_zero
zero_add := Int.zero_add
neg_add_cancel := Int.add_left_neg
nsmul := (· * ·)
nsmul_zero := Int.zero_mul
nsmul_succ n x := show (n + 1 : ℤ) * x = n * x + x by rw [Int.add_mul, Int.one_mul]
zsmul := (· * ·)
zsmul_zero' := Int.zero_mul
zsmul_succ' m n := by simp only [natCast_succ, Int.add_mul, Int.add_comm, Int.one_mul]
zsmul_neg' m n := by simp only [negSucc_eq, natCast_succ, Int.neg_mul]
sub_eq_add_neg _ _ := Int.sub_eq_add_neg
