eq_of_fst_eq_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive VAddAntidiagonal.eq_of_fst_eq_fst]
theorem eq_of_fst_eq_fst (h : (x : G × P).fst = (y : G × P).fst) : x = y :=
  Subtype.ext <| Prod.ext h <| fst_eq_fst_iff_snd_eq_snd.1 h

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