leftCosetEquivalence_equiv_fst — Mathlib

English

The first component of the complement equivalence corresponds to a LeftCosetEquivalence between the subgroup K and elements g.

Русский

Первая компонента эквивалентности дополнения соответствует LeftCosetEquivalence для подгруппы K и элементов g.

LaTeX

$$$ (\text{LeftCosetEquivalence} K\; g_1\; g_2) \iff (hSK.equiv g_1).fst = (hSK.equiv g_2).fst. $$$

Lean4

theorem leftCosetEquivalence_equiv_fst (g : G) : LeftCosetEquivalence K g ((hSK.equiv g).fst : G) := by
  -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
  rw [equiv_fst_eq_mul_inv]; simp [LeftCosetEquivalence, leftCoset_eq_iff]

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