instSMulCommClass_closedBall_circle

Mathlib.Analysis.Complex.UnitDisc.Basic

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

English

There is SMulCommClass (closedBall 0 1) Circle UnitDisk: actions commute between closedBall and Circle on UnitDisk.

Русский

Существует SMulCommClass (closedBall 0 1) Circle UnitDisk: действия совместимы.

LaTeX

$$$ SMulCommClass (closedBall 0 1) Circle UnitDisk $$$

Lean4

instance instSMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : ℂ) 1) Circle 𝔻 :=
  SMulCommClass.symm _ _ _

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

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

Разделы

Аффилиация

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