Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 19:03 382acc15

View on Github →

feat(geometry/manifold): generalize some lemmas from smooth to cont_mdiff (#15560) Also add *_within_at, *_at, and *_on versions.

Estimated changes

added theorem cont_mdiff.mul
added theorem cont_mdiff_at.mul
added theorem cont_mdiff_finprod
added theorem cont_mdiff_finset_prod
added theorem cont_mdiff_on.mul
modified theorem smooth.mul
added theorem smooth_at.mul
added theorem smooth_at_finset_prod'
added theorem smooth_at_finset_prod
modified theorem smooth_finprod
modified theorem smooth_finprod_cond
modified theorem smooth_finset_prod'
modified theorem smooth_finset_prod
modified theorem smooth_on.mul
added theorem smooth_on_finset_prod'
added theorem smooth_on_finset_prod
added theorem smooth_within_at.mul
added theorem cont_mdiff.smul
added theorem cont_mdiff_at.smul
added theorem cont_mdiff_on.smul
modified theorem smooth.smul
modified theorem smooth_at.smul
deleted theorem smooth_at_univ
added theorem smooth_on.smooth_at
modified theorem smooth_on.smul
modified theorem smooth_on_univ
added theorem smooth_within_at.smul
added theorem smooth_within_at_univ