English
The rationals with addition form an additive commutative group.
Русский
К рациональным числам по сложению применяется структура аддитивной коммутативной группы.
LaTeX
$$$(\mathbb{Q}, +)$ is an additive commutative group.$$
Lean4
instance addCommGroup : AddCommGroup ℚ where
zero := 0
add := (· + ·)
neg := Neg.neg
zero_add := Rat.zero_add
add_zero := Rat.add_zero
add_comm := Rat.add_comm
add_assoc := Rat.add_assoc
neg_add_cancel := Rat.neg_add_cancel
sub_eq_add_neg := Rat.sub_eq_add_neg
nsmul := (· * ·)
zsmul := (· * ·)
nsmul_zero := Rat.zero_mul
nsmul_succ n
q := by
change ((n + 1 : Int) : Rat) * q = _
rw [Rat.intCast_add, Rat.add_mul, Rat.intCast_one, Rat.one_mul]
rfl
zsmul_zero' := Rat.zero_mul
zsmul_succ' _ _ := by simp [Rat.add_mul]
zsmul_neg' _ _ := by rw [Int.negSucc_eq, Rat.intCast_neg, Rat.neg_mul]; rfl
