instSMulCommClass_closedBall'

Mathlib.Analysis.Complex.UnitDisc.Basic

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

English

The symmetric SMulCommClass between UnitDisk and closedBall(0,1) holds: UnitDisk smul closedBall and closedBall smul UnitDisk commute.

Русский

Симметричная SMulCommClass между UnitDisk и closedBall держится: действия совместимы.

LaTeX

$$$ SMulCommClass UnitDisk (closedBall(0,1)) 𝔻 $$$

Lean4

instance instSMulCommClass_closedBall' : SMulCommClass 𝔻 (closedBall (0 : ℂ) 1) 𝔻 :=
  SMulCommClass.symm _ _ _

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

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

Разделы

Аффилиация

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