times_cont_diff): inversion is smooth (#3639)

Commit

5 years ago

feat(analysis/calculus/times_cont_diff): inversion is smooth (#3639) At an invertible element of a complete normed algebra, the inversion operation is smooth.

Author

hrmacbeth

Parents

d3de289a

mathlib3 fc65ba0d - feat(analysis/calculus/times_cont_diff): inversion is smooth (#3639)

mathlib3
fc65ba0d - feat(analysis/calculus/times_cont_diff): inversion is smooth (#3639)