instInvolutiveNeg — Mathlib

English

For every n, Fin(n) with negation is an involutive negation: neg(neg x) = x.

Русский

Для любого n Fin(n) с операцией отрицания является1 инволютивное отрицание: отрицание двойного отрицания даёт исходное число.

LaTeX

$$$\\forall n\\, (\\mathrm{Fin}(n), \\mathrm{neg})\\ \\,\\text{is an involutive negation: } \\mathrm{neg}(\\mathrm{neg}(x))=x$$$

Lean4

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

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