instIsTopologicalGroup

Mathlib.Analysis.Complex.Circle

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

English

The circle carries a natural topological group structure (coming from multiplication on the unit circle).

Русский

У окружности естественная топологическая групповая структура (происходит от умножения на единичной окружности).

LaTeX

$$$$ IsTopologicalGroup(Circle). $$$$

Lean4

instance : IsTopologicalGroup Circle :=
  Metric.sphere.instIsTopologicalGroup

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

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

Разделы

Аффилиация

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