instIsScalarTower — Mathlib

English

If SMul ℂ α and SMul ℂ β and SMul α β and IsScalarTower ℂ α β hold, then Circle α β is a scalar tower.

Русский

Если выполняются условия скалярной башни, то Circle α β образует скалярную башню.

LaTeX

$$$$ \\text{IsScalarTower Circle } \\alpha \\beta, $$$$

Lean4

instance instIsScalarTower [SMul ℂ α] [SMul ℂ β] [SMul α β] [IsScalarTower ℂ α β] : IsScalarTower Circle α β :=
  Submonoid.isScalarTower _

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