equiv_mul_right — Mathlib

English

The equality of first coordinates for two elements is equivalent to a LeftCosetEquivalence with respect to K.

Русский

Равенство первых координат двух элементов эквивалентно левой косет-эквивалентности по K.

LaTeX

$$$ (hSK.equiv g_1).fst = (hSK.equiv g_2).fst \iff LeftCosetEquivalence K g_1 g_2. $$$

Lean4

theorem equiv_mul_right (g : G) (k : K) : hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) :=
  by
  have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst :=
    hSK.equiv_fst_eq_iff_leftCosetEquivalence.2 (by simp [LeftCosetEquivalence, leftCoset_eq_iff])
  ext
  · rw [this]
  · rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]

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