instElemOrbit_1 — Mathlib

English

There is a natural induced action of G on each orbit of α.

Русский

Для каждой орбиты α существует естественное действие G на орбиту.

LaTeX

$$instance (x : orbitRel.Quotient G α) : MulAction G x.orbit$$

Lean4

@[to_additive]
instance (x : orbitRel.Quotient G α) : MulAction G x.orbit
    where
  smul g := (orbitRel.Quotient.mapsTo_smul_orbit g x).restrict _ _ _
  one_smul a := Subtype.ext (one_smul G (a : α))
  mul_smul g g' a' := Subtype.ext (mul_smul g g' (a' : α))

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