circleAction

Mathlib.Analysis.Complex.UnitDisc.Basic

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

English

There is a multiplicative action of the circle on 𝔻 by multiplication.

Русский

Существует круговое действие на 𝔻 умножением.

LaTeX

$$$ \\forall \\theta \\in Circle, \\ z \\in 𝔻,\\ \\theta \\cdot z \\in 𝔻. $$$

Lean4

instance circleAction : MulAction Circle 𝔻 :=
  mulActionSphereBall

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

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

Разделы

Аффилиация

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