instElemOrbit — Mathlib

English

There is a natural action of M on the elements of the orbit of a, induced from the action on α.

Русский

Существует естественное действие M на элементы орбиты a, наследуемое от действия на α.

LaTeX

$$$\text{MulAction}_{M}(\operatorname{orbit}(M,a).\text{Elem})$ is well-defined with smul defined by restrictions.$$

Lean4

@[to_additive]
instance {a : α} : MulAction M (orbit M a)
    where
  smul m := (mapsTo_smul_orbit m a).restrict _ _ _
  one_smul m := Subtype.ext (one_smul M (m : α))
  mul_smul m m' a' := Subtype.ext (mul_smul m m' (a' : α))

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