instChartedSpace

Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

URI: https://scilib.ai/kg/mathlib#Units.instChartedSpace

English

The group of units of a complete normed ring forms a Lie group (with corners).

Русский

Группа единиц полного нормированного кольца образует Ли-группу (с углами).

LaTeX

$$The group $R^{\times}$ is a LieGroup with modelWithCorners; the multiplication and inversion maps are smooth.$$

Lean4

instance : ChartedSpace R Rˣ :=
  isOpenEmbedding_val.singletonChartedSpace

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

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

Разделы

Аффилиация

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