mathlib3

3077b72c - feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals (#16446)

feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals (#16446) This takes the existing norm structures on quotients of additive groups and transfers it along the definitional equality to quotients of modules by submodules and quotients of rings by ideals. In addition, this puts the extra norm structures on these objects where appropriate including `complete_space`, `normed_space`, `semi_normed_comm_ring`, `normed_comm_ring` and `normed_algebra`. - [x] depends on: #16368