mathlib3

db9842c8 - feat(analysis/calculus/times_cont_diff): inversion of continuous linear maps is smooth (#4185)

feat(analysis/calculus/times_cont_diff): inversion of continuous linear maps is smooth (#4185) - Introduce an `inverse` function on the space of continuous linear maps between two Banach spaces, which is the inverse if the map is a continuous linear equivalence and zero otherwise. - Prove that this function is `times_cont_diff_at` each `continuous_linear_equiv`. - Some of the constructions used had been introduced in #3282 and placed in `analysis.normed_space.operator_norm` (normed spaces); they are moved to the earlier file `topology.algebra.module` (topological vector spaces). Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>