instAddLeftCancelSemigroup — Mathlib

English

Fin(n) with addition is an AddLeftCancelSemigroup.

Русский

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

LaTeX

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

Lean4

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

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