Commit 2020-08-02 03:20 fc65ba0d

View on Github →

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

Estimated changes

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff.comp_times_cont_diff_at

added theorem times_cont_diff_at.comp

added theorem times_cont_diff_at_inverse

added theorem times_cont_diff_at_succ_iff_has_fderiv_at

Modified src/analysis/normed_space/bounded_linear_maps.lean

added theorem continuous_linear_map.lmul_left_right_is_bounded_bilinear

Modified src/analysis/normed_space/operator_norm.lean

modified def continuous_linear_map.lmul_left

modified theorem continuous_linear_map.lmul_left_apply

added theorem continuous_linear_map.lmul_left_norm

added def continuous_linear_map.lmul_left_right

added theorem continuous_linear_map.lmul_left_right_apply

added theorem continuous_linear_map.lmul_left_right_norm_le

modified def continuous_linear_map.lmul_right

modified theorem continuous_linear_map.lmul_right_apply

added theorem continuous_linear_map.lmul_right_norm

Modified src/analysis/normed_space/units.lean

added theorem units.nhds

Modified src/ring_theory/algebra.lean

added def algebra.lmul_left_right

added theorem algebra.lmul_left_right_apply