stabilizer_of_subMul — Mathlib

English

The orbit relation on p coincides with the comap of the ambient orbitRel on M via the inclusion map.

Русский

Отношение орбит на p совпадает с прообразом отношения орбит в M через включение.

LaTeX

$$$ \\text{orbitRel}_R(p) = \\big( \\text{orbitRel}_R(M) \\big) \\mathrel{\\text{comap}} \\text{Subtype.val} $$$

Lean4

/-- Stabilizers in group SubMulAction coincide with stabilizers in the ambient space -/
@[to_additive]
theorem stabilizer_of_subMul {p : SubMulAction R M} (m : p) :
    MulAction.stabilizer R m = MulAction.stabilizer R (m : M) :=
  by
  rw [← Subgroup.toSubmonoid_inj]
  exact stabilizer_of_subMul.submonoid m

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