Commit 2020-09-20 21:53 db9842c8

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).