orbit_subgroup_eq_rightCoset — Mathlib

English

For any a in α and subgroup s of α, the orbit of a under s equals the left coset a s.

Русский

Для любой a в группе и подгруппы s верно, что орбита a под действием s равна левой косете a s.

LaTeX

$$$\mathrm{Orb}_{s}(a) = a\,s$$$

Lean4

@[to_additive]
theorem orbit_subgroup_eq_rightCoset (a : α) : MulAction.orbit s a = op a • s :=
  Set.ext fun _b => ⟨fun ⟨c, d⟩ => ⟨c, c.2, d⟩, fun ⟨c, d, e⟩ => ⟨⟨c, d⟩, e⟩⟩

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