contMDiff_val — Mathlib

English

The embedding of units into the base ring is a C^n map between manifolds.

Русский

Встраивание единиц в кольцо — отображение класса C^n между многообразиями.

LaTeX

$$contMDiff_val : ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) n (val : Rˣ → R)$$

Lean4

/-- For a complete normed ring `R`, the embedding of the units `Rˣ` into `R` is a `C^n` map between
manifolds. -/
theorem contMDiff_val : ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) n (val : Rˣ → R) :=
  contMDiff_isOpenEmbedding Units.isOpenEmbedding_val

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