isScalarTower_closedBall — Mathlib

English

IsScalarTower (closedBall 0 1) 𝔻 Complex.UnitDisc on Complex.UnitDisc: compatibility of successive actions holds: (a • b) • x = a • (b • x).

Русский

IsScalarTower (closedBall 0 1) 𝔻 Complex.UnitDisc на Complex.UnitDisc: совместимость последовательных действий.

LaTeX

$$$ IsScalarTower (closedBall 0 1) 𝔻 Complex.UnitDisc $$$

Lean4

instance isScalarTower_closedBall : IsScalarTower (closedBall (0 : ℂ) 1) 𝔻 𝔻 :=
  isScalarTower_closedBall_ball_ball

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