instSMulCommClass_left — Mathlib

English

If ℂ acts on β and α acts on β with SMulCommClass ℂ α β, then Circle α β inherits SMulCommClass Circle α β.

Русский

Если ℂ действует на β и α действует наβ с SMulCommClass ℂ α β, то Circle α β наследует SMulCommClass Circle α β.

LaTeX

$$$$ \\text{SMulCommClass Circle } \\alpha \\beta, \\text{ given } [SMul ℂ β], [SMul α β], [SMulCommClass ℂ α β]. $$$$

Lean4

instance instSMulCommClass_left [SMul ℂ β] [SMul α β] [SMulCommClass ℂ α β] : SMulCommClass Circle α β :=
  Submonoid.smulCommClass_left _

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