Commit 2023-06-24 15:15 392ed755

View on Github →

feat: port Geometry.Manifold.Algebra.Monoid (#5438)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/Algebra/Monoid.lean

added theorem ContMDiff.mul

added theorem ContMDiffOn.mul

added theorem ContMDiffWithinAt.mul

added theorem L_apply

added theorem L_mul

added theorem R_apply

added theorem R_mul

added structure SmoothAddMonoidMorphism

added structure SmoothMonoidMorphism

added theorem contMDiffAt_finset_prod'

added theorem contMDiffAt_finset_prod

added theorem contMDiffOn_finset_prod'

added theorem contMDiffOn_finset_prod

added theorem contMDiffWithinAt_finset_prod'

added theorem contMDiffWithinAt_finset_prod

added theorem contMDiff_finprod

added theorem contMDiff_finprod_cond

added theorem contMDiff_finset_prod'

added theorem contMDiff_finset_prod

added theorem continuousMul_of_smooth

added theorem smoothAt_finset_prod'

added theorem smoothAt_finset_prod

added def smoothLeftMul

added theorem smoothLeftMul_one

added theorem smoothOn_finset_prod'

added theorem smoothOn_finset_prod

added def smoothRightMul

added theorem smoothRightMul_one

added theorem smoothWithinAt_finset_prod'

added theorem smoothWithinAt_finset_prod

added theorem smooth_finprod

added theorem smooth_finprod_cond

added theorem smooth_finset_prod'

added theorem smooth_finset_prod

added theorem smooth_mul

added theorem smooth_mul_left

added theorem smooth_mul_right

added theorem smooth_pow