Commit 2023-12-13 09:43 395e8530

feat(Geometry/Manifold/Instances/UnitsOfNormedAlgebra): Lie group structure (#8397) Port of [mathlib#15763](https://github.com/leanprover-community/mathlib/pull/15763) We complete the construction of the Lie group of units of a complete normed ring. To show that multiplication and inversion are smooth, we add some more lemmas:

1. For a manifold M whose chart structure is induced by an open embedding from M to H, the open embedding itself is a smooth manifold map.
2. The inverse of this open embedding is smooth on its range.
3. For a manifold map f : M → M' whose target space M' has a chart structure induced by an open embedding e' : M' → H', if e' ∘ f is smooth, then f is smooth. Lemmas previously not ported are now ported:
4. open_embedding.to_local_homeomorph_left_inv
5. open_embedding.to_local_homeomorph_right_inv