mathlib3

396a764f - feat(analysis/calculus/fderiv): inversion is differentiable (#3510)

feat(analysis/calculus/fderiv): inversion is differentiable (#3510) At an invertible element `x` of a complete normed algebra, the inversion operation of the algebra is Fréchet-differentiable, with derivative `λ t, - x⁻¹ * t * x⁻¹`.