Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-22 01:22 d98479aa

View on Github →

feat(analysis/calculus/cont_diff): generalize mul lemmas to a normed algebra (#15595) Also add lemmas about finset.prod.

Estimated changes

modified theorem cont_diff.div_const
modified theorem cont_diff.mul
modified theorem cont_diff.pow
modified theorem cont_diff_at.div_const
modified theorem cont_diff_at.mul
modified theorem cont_diff_at.pow
added theorem cont_diff_at_prod'
added theorem cont_diff_at_prod
modified theorem cont_diff_mul
modified theorem cont_diff_on.div_const
modified theorem cont_diff_on.mul
modified theorem cont_diff_on.pow
added theorem cont_diff_on_prod'
added theorem cont_diff_on_prod
added theorem cont_diff_prod'
added theorem cont_diff_prod
modified theorem cont_diff_within_at.mul
modified theorem cont_diff_within_at.pow