instAddRightCancelSemigroup — Mathlib

English

Fin(n) with addition is an AddRightCancelSemigroup.

Русский

Fin(n) с операцией сложения образует AddRightCancelSemigroup.

LaTeX

$$$\\forall n\\, \\operatorname{AddRightCancelSemigroup}(\\mathrm{Fin}(n))$$$

Lean4

/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instAddRightCancelSemigroup (n : ℕ) : AddRightCancelSemigroup (Fin n) :=
  { Fin.addCommSemigroup n, Fin.instIsCancelAdd n with }

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