Commit 2021-04-14 18:40 27157699

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? -/
}