addCommSemigroup — Mathlib

English

For every natural n, Fin(n) with addition modulo n forms an AddCommSemigroup.

Русский

Для каждого натурального n множество Fin(n) с операцией сложения по модулю n образует аддитивную коммутативную полугруппу.

LaTeX

$$$\\operatorname{AddCommSemigroup}(\\mathrm{Fin}(n))$$$

Lean4

instance addCommSemigroup (n : ℕ) : AddCommSemigroup (Fin n)
    where
  add_assoc := by simp [add_def, Nat.add_assoc]
  add_comm := by simp [add_def, Nat.add_comm]

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