instSubsingletonHasAntidiagonal — Mathlib

English

All HasAntidiagonal structures on any AddMonoid A are equal; in particular, HasAntidiagonal A forms a subsingleton type.

Русский

Структуры HasAntidiagonal на любом AddMonoid A равны между собой; имеет место подсложность типа HasAntidiagonal.

LaTeX

$$$\\text{Subsingleton}(\\text{HasAntidiagonal } A)$ for every AddMonoid A$$

Lean4

/-- All `HasAntidiagonal` instances are equal -/
instance [AddMonoid A] : Subsingleton (HasAntidiagonal A) where
  allEq := by
    rintro ⟨a, ha⟩ ⟨b, hb⟩
    congr with n xy
    rw [ha, hb]
      -- The goal of this lemma is to allow to rewrite antidiagonal
      -- when the decidability instances obsucate Lean

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