rightCosetEquivalence_equiv_snd — Mathlib

English

The second component corresponds to RightCosetEquivalence of H with respect to g1 and g2.

Русский

Вторая компонента соответствует RightCosetEquivalence подгруппа H по элементам g1 и g2.

LaTeX

$$$ (\text{RightCosetEquivalence} H\; g_1\; g_2) \iff (hHT.equiv g_1).snd = (hHT.equiv g_2).snd. $$$

Lean4

theorem rightCosetEquivalence_equiv_snd (g : G) : RightCosetEquivalence H g ((hHT.equiv g).snd : G) := by
  -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
  rw [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul]; simp

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