instIsManifoldModelWithCornersSelf

English

The units of a complete normed ring form a manifold (with corners) with respect to the model-with-corners structure.

Русский

Единицы полного нормированного кольца образуют многообразие (с углами) в зависимости от модели с углами.

LaTeX

$$IsManifold (modelWithCornersSelf 𝕜 R) n (Units R)$$

Lean4

instance : IsManifold 𝓘(𝕜, R) n Rˣ :=
  isOpenEmbedding_val.isManifold_singleton

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