closedBallAction

Mathlib.Analysis.Complex.UnitDisc.Basic

URI: https://scilib.ai/kg/mathlib#Complex.UnitDisc.closedBallAction

English

The closed unit ball in ℂ acts on 𝔻 by multiplication.

Русский

Замкнутый единичный шар в ℂ действует на 𝔻 умножением.

LaTeX

$$$ \\forall z \\in \\overline{B}(0,1),\\ x \\in 𝔻,\\ z x \\in 𝔻. $$$

Lean4

instance closedBallAction : MulAction (closedBall (0 : ℂ) 1) 𝔻 :=
  mulActionClosedBallBall

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru