instMulAction — Mathlib

English

If there is a MulAction of ℂ on α, then Circle acts on α via the restricted action from ℂ.

Русский

Если имеется умножение ℂ на α, то Circle действует на α через ограниченное действие ℂ.

LaTeX

$$$$ [MulAction Circle \\alpha], \\; \\text{defined by restriction of } [MulAction \\mathbb{C} \\alpha]. $$$$

Lean4

instance instMulAction [MulAction ℂ α] : MulAction Circle α :=
  Submonoid.mulAction _

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