fst_eq_fst_iff_snd_eq_snd — Mathlib

English

For elements x,y of the MulAntidiagonal, equality of first coordinates implies equality of second coordinates and vice versa (under cancellation conditions).

Русский

В MulAntidiagonal равенство первых координат влечет за собой равенство вторых координат и наоборот (при некоторых условиях отмены).

LaTeX

$$Theorem: (x.1 = y.1) ↔ (x.2 = y.2) for x,y ∈ (s.mulAntidiagonal t a).Elem under commutative cancellative structure.$$

Lean4

@[to_additive Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd]
theorem fst_eq_fst_iff_snd_eq_snd : (x : α × α).1 = (y : α × α).1 ↔ (x : α × α).2 = (y : α × α).2 :=
  ⟨fun h =>
    mul_left_cancel
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm,
    fun h =>
    mul_right_cancel
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm⟩

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