Commit 2025-10-17 16:01 52271671

View on Github →

feat: add module instance to ContDiffMapSupportedIn (#30198) Add a module instance for the type ContDiffMapSupportedIn of n-times continuously differentiable maps supported in a fixed compact.

Estimated changes

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

added theorem ContDiffMapSupportedIn.add_apply

added def ContDiffMapSupportedIn.coeHom

added theorem ContDiffMapSupportedIn.coeHom_injective

added theorem ContDiffMapSupportedIn.coe_add

added theorem ContDiffMapSupportedIn.coe_coeHom

added theorem ContDiffMapSupportedIn.coe_neg

added theorem ContDiffMapSupportedIn.coe_smul

added theorem ContDiffMapSupportedIn.coe_sub

added theorem ContDiffMapSupportedIn.coe_zero

added theorem ContDiffMapSupportedIn.neg_apply

added theorem ContDiffMapSupportedIn.smul_apply

added theorem ContDiffMapSupportedIn.sub_apply

added theorem ContDiffMapSupportedIn.toBoundedContinuousFunction_apply

added theorem ContDiffMapSupportedIn.zero_apply

Modified Mathlib/Data/Set/Function.lean

added theorem Set.EqOn.comp_left₂