left_quotientAction — Mathlib

English

For any subgroup H of G, there is a natural action of the left coset representatives on G/H given by b · (aH) = (b a)H for b in the acting group.

Русский

Для подгруппы H ⊆ G существует естественное левое действие на множествах левых косет G/H: b · (aH) = (b a)H для любого b.

LaTeX

$$$\\forall b \\in \\beta,\\; \\forall aH \\in G/H:\\; b \\cdot (aH) = (b\\cdot a)H$$$

Lean4

@[to_additive]
instance left_quotientAction : QuotientAction α H :=
  ⟨fun _ _ _ _ => by rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]⟩

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