addCommGroup — Mathlib

English

The complex numbers form an additive commutative group under standard addition.

Русский

Комплексные числа образуют аддитивную коммутативную группу относительно обычного сложения.

LaTeX

$$$\\text{AbelianGroup}(\\mathbb{C}, +)$$$

Lean4

instance addCommGroup : AddCommGroup ℂ :=
  { zero := (0 : ℂ)
    add := (· + ·)
    neg := Neg.neg
    sub := Sub.sub
    nsmul := fun n z => n • z
    zsmul := fun n z => n • z
    zsmul_zero' := by intros; ext <;> simp [smul_re, smul_im]
    nsmul_zero := by intros; ext <;> simp [smul_re, smul_im]
    nsmul_succ := by intros; ext <;> simp [smul_re, smul_im] <;> ring
    zsmul_succ' := by intros; ext <;> simp [smul_re, smul_im] <;> ring
    zsmul_neg' := by intros; ext <;> simp [smul_re, smul_im] <;> ring
    add_assoc := by intros; ext <;> simp <;> ring
    zero_add := by intros; ext <;> simp
    add_zero := by intros; ext <;> simp
    add_comm := by intros; ext <;> simp <;> ring
    neg_add_cancel := by intros; ext <;> simp }

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