Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 02:07 94fa9058

View on Github →

feat(analysis/calculus/times_cont_diff): differentiability of field inverse (#4795)

Estimated changes

Modified src/algebra/field.lean

added theorem inverse_eq_has_inv

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff.div

added theorem times_cont_diff.pow

modified theorem times_cont_diff_at.comp

added theorem times_cont_diff_at.comp_times_cont_diff_within_at

added theorem times_cont_diff_at.congr_of_eventually_eq

added theorem times_cont_diff_at.div

added theorem times_cont_diff_at.inv

added theorem times_cont_diff_at_id

added theorem times_cont_diff_at_inv

added theorem times_cont_diff_on_id

added theorem times_cont_diff_within_at.congr_nhds

deleted theorem times_cont_diff_within_at.continuous_within_at'

added theorem times_cont_diff_within_at.div

added theorem times_cont_diff_within_at.inv

added theorem times_cont_diff_within_at.mono_of_mem

added theorem times_cont_diff_within_at_congr_nhds

added theorem times_cont_diff_within_at_id

Modified src/geometry/manifold/times_cont_mdiff.lean

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.one_def

Modified src/topology/continuous_on.lean

added theorem continuous_within_at.mono_of_mem

added theorem continuous_within_at_insert_self

modified theorem continuous_within_at_singleton

added theorem continuous_within_at_union

added theorem insert_mem_nhds_within_insert

modified theorem mem_nhds_within_insert

added theorem nhds_within_insert

added theorem nhds_within_singleton