equiv_mul_left — Mathlib

English

Two first coordinates are equal if and only if the corresponding elements lie in the same left coset of K.

Русский

Две первые координаты равны тогда и только тогда, когда соответствующие элементы лежат в одном левом косете K.

LaTeX

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

Lean4

theorem equiv_mul_left (h : H) (g : G) : hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) :=
  by
  have : (hHT.equiv (h * g)).2 = (hHT.equiv g).2 := hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 ?_
  · ext
    · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
    · rw [this]
  · simp [RightCosetEquivalence, ← smul_smul]

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