eq_of_snd_eq_snd — Mathlib

English

If two elements x,y of mulAntidiagonal have equal second coordinates, then x = y.

Русский

Если x и y из mulAntidiagonal s t a имеют одинаковые вторые координаты, то x = y.

LaTeX

$$For x,y ∈ (s.mulAntidiagonal t a).Elem, if x.val.snd = y.val.snd then x = y.$$

Lean4

@[to_additive Set.AddAntidiagonal.eq_of_snd_eq_snd]
theorem eq_of_snd_eq_snd (h : (x : α × α).snd = (y : α × α).snd) : x = y :=
  Subtype.ext <| Prod.ext (fst_eq_fst_iff_snd_eq_snd.2 h) h

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