instSMul

Mathlib.Analysis.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Circle.instSMul

English

The unit circle acts on any α by restricting the ℂ-action: z • a = z a for z ∈ Circle, a ∈ α.

Русский

Единичная окружность действует на любом α, ограничивая действие ℂ: z • a = z a, где z ∈ Circle, a ∈ α.

LaTeX

$$$$ z \\cdot a = (z) a \\quad \\text{for } z \\in \\mathrm{Circle}, a \\in \\alpha, $$$$

Lean4

instance instSMul [SMul ℂ α] : SMul Circle α :=
  Submonoid.smul _

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

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

Разделы

Аффилиация

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