mathlib3

27157699 - feat(geometry/manifold/instances/units_of_normed_algebra): the units of a normed algebra are a topological group and a smooth manifold (#6981)

feat(geometry/manifold/instances/units_of_normed_algebra): the units of a normed algebra are a topological group and a smooth manifold (#6981) I decided to make a small PR now with only a partial result because Heather suggested proving GL^n is a Lie group on Zulip, and I wanted to share the work I did so that whoever wants to take over the task does not have to start from scratch. Most of the ideas in this PR are by @hrmacbeth, as I was planning on doing a different proof, but I agreed Heather's one was better. What remains to do in a future PR to prove GLn is a Lie group is to add and prove the following instance to the file `geometry/manifold/instances/units_of_normed_algebra.lean`: ``` instance units_of_normed_algebra.lie_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {R : Type*} [normed_ring R] [normed_algebra 𝕜 R] [complete_space R] : lie_group (model_with_corners_self 𝕜 R) (units R) := { smooth_mul := begin sorry, end, smooth_inv := begin sorry, end, ..units_of_normed_algebra.smooth_manifold_with_corners, /- Why does it not find the instance alone? -/ } ``` Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>