instIsCancelAdd — Mathlib

English

For Fin(n) the additive structure is cancelative on both sides: a+b=a+c implies b=c, and a+c=a+b implies c=b.

Русский

Для Fin(n) сложение имеет свойство отмены слева и справа: если a+b=a+c, то b=c, и если a+c=a+b, то c=b.

LaTeX

$$$\\forall n\\, \\text{Fin}(n)\\text{ isCancelAdd}$$$

Lean4

/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instIsCancelAdd (n : ℕ) : IsCancelAdd (Fin n)
    where
  add_left_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_left_cancel
  add_right_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_right_cancel

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