Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-13 13:57 d608fc5d

View on Github →

feat(analysis/calculus/fderiv/mul): derivative of inverse in division rings (#19127)

Estimated changes

Modified src/analysis/calculus/fderiv/mul.lean

added theorem differentiable.inv'

added theorem differentiable.inverse

added theorem differentiable_at.inv'

added theorem differentiable_at.inverse

added theorem differentiable_at_inv'

modified theorem differentiable_at_inverse

added theorem differentiable_on.inv'

added theorem differentiable_on.inverse

added theorem differentiable_on_inv'

added theorem differentiable_on_inverse

added theorem differentiable_within_at.inv'

added theorem differentiable_within_at.inverse

added theorem differentiable_within_at_inv'

added theorem differentiable_within_at_inverse

added theorem fderiv_inv'

added theorem fderiv_within_inv'

added theorem has_fderiv_at_inv'

Modified src/analysis/normed_space/spectrum.lean