instSMulCommClass_circle'

Mathlib.Analysis.Complex.UnitDisc.Basic

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

English

The symmetric SMulCommClass between UnitDisk and Circle holds: 𝔻 smul Circle and Circle smul 𝔻 commute on UnitDisk.

Русский

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

LaTeX

$$$ SMulCommClass 𝔻 Circle 𝔻 $$$

Lean4

instance instSMulCommClass_circle' : SMulCommClass 𝔻 Circle 𝔻 :=
  SMulCommClass.symm _ _ _

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

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

Разделы

Аффилиация

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