eq_of_snd_eq_snd — Mathlib

English

If the second coordinates of two elements of smulAntidiagonal are equal, then the two elements are equal.

Русский

Если вторые координаты двух элементов smulAntidiagonal совпадают, то элементы равны.

LaTeX

$$$\forall x,y \in (s.smulAntidiagonal t a).Elem,\; x.snd = y.snd \rightarrow x = y$$$

Lean4

@[to_additive VAddAntidiagonal.eq_of_snd_eq_snd]
theorem eq_of_snd_eq_snd (h : (x : G × P).snd = (y : G × P).snd) : x = y :=
  Subtype.ext <| Prod.ext (fst_eq_fst_iff_snd_eq_snd.2 h) h

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