fst_eq_fst_iff_snd_eq_snd — Mathlib

English

In the smulAntidiagonal context with an orderedCancelSMul, equality of the first coordinates implies equality of the second coordinates and vice versa.

Русский

В контексте smulAntidiagonal с упорядоченным аннулированием умножения равенство первых координат эквивалентно равенству вторых координат, и наоборот.

LaTeX

$$$(x: (s.\,smulAntidiagonal t a).\text{Elem}).1 = (y:(s.\,smulAntidiagonal t a).\text{Elem}).1 \iff (x).2=(y).2$$$

Lean4

@[to_additive VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd]
theorem fst_eq_fst_iff_snd_eq_snd : (x : G × P).1 = (y : G × P).1 ↔ (x : G × P).2 = (y : G × P).2 :=
  ⟨fun h =>
    IsCancelSMul.left_cancel _ _ _
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm,
    fun h =>
    IsCancelSMul.right_cancel _ _ _
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm⟩

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