hasAntidiagonal_congr — Mathlib

English

If two HasAntidiagonal structures exist on A, their antidiagonal relations coincide.

Русский

Если существуют две структуры HasAntidiagonal на A, их антидиагональные отношения совпадают.

LaTeX

$$$\\forall A,\\; [\\text{HasAntidiagonal } A]\\text{ } H_1.antidiagonal = H_2.antidiagonal$$$

Lean4

theorem hasAntidiagonal_congr (A : Type*) [AddMonoid A] [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] :
    H1.antidiagonal = H2.antidiagonal := by congr!; subsingleton

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