isPretransitive_quotient — Mathlib

English

The left action of G on G/H is transitive: any two cosets lie in the same orbit.

Русский

Действие G на смежных косетах G/H предварительно Transitive: для любых coset xH, yH существует g ∈ G такой, что g·(xH) = yH.

LaTeX

$$IsPretransitive G (G ⧸ H) with exists_smul_eq$$

Lean4

@[to_additive]
instance isPretransitive_quotient (G) [Group G] (H : Subgroup G) : IsPretransitive G (G ⧸ H) where
  exists_smul_eq := by {
    rintro ⟨x⟩ ⟨y⟩
    refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
    simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]
  }

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