instSMul — Mathlib

English

There is a natural SMul action of the opposite subgroup H^{op} on G, coming from restricting the ambient group multiplication to the submonoid H^{op}.

Русский

Существет естественное действие SMul элемента противоположной подгруппы H^{op} на G, получаемое ограничением умножения в группе к подмонойду H^{op}.

LaTeX

$$instSMul (H : Subgroup G) : SMul H.op G$$

Lean4

@[to_additive]
instance instSMul (H : Subgroup G) : SMul H.op G :=
  Submonoid.smul ..

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