Units.contMDiff_val

theorem Units.contMDiff_val : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {𝕜 : Type u_2} [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAlgebra 𝕜 R] {m : ℕ∞}, ContMDiff (modelWithCornersSelf 𝕜 R) (modelWithCornersSelf 𝕜 R) m Units.val

The theorem `Units.contMDiff_val` states that in the case of a complete normed ring `R`, the operation of embedding the units of `R` (denoted `Rˣ`) back into `R` is a smooth map between manifolds. This is stated for all `R` and `𝕜`, where `R` is a type having a normed ring structure and is a complete space, and `𝕜` is a type equipped with a non-trivially normed field structure and a normed algebra structure over `R`. The smoothness of the map is considered with respect to the model with corners on `R` associated with `𝕜`, denoted `modelWithCornersSelf 𝕜 R`, and is true for all smoothness classes `m`.

More concisely: The embedding of the units of a complete normed ring `R` into `R` is a smooth map between manifolds with respect to the model with corners on `R` associated with a non-trivially normed field `𝕜` for all smoothness classes `m`.