equiv_mul_right_of_mem — Mathlib

English

The second component equals s^{-1} g whenever g = s t with s ∈ S, t ∈ T; equivalently, t = s^{-1} g.

Русский

Вторая компонента равна s^{-1} g, если g = s t с s ∈ S, t ∈ T; следовательно, t = s^{-1} g.

LaTeX

$$$ (hST.equiv g).snd = ( (hST.equiv g).fst )^{-1} g. $$$

Lean4

theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) :
    hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * ⟨k, h⟩) :=
  equiv_mul_right _ g ⟨k, h⟩

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