Commit 2025-10-31 13:29 eba35bfd

View on Github →

chore(ContDiffSupportedIn): use simps to auto-generate basic API (#30659) Follow-up to #30198.

Estimated changes

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

deleted def ContDiffMapSupportedIn.Simps.apply

added def ContDiffMapSupportedIn.Simps.coe

deleted theorem ContDiffMapSupportedIn.coe_add

deleted theorem ContDiffMapSupportedIn.coe_neg

deleted theorem ContDiffMapSupportedIn.coe_smul

deleted theorem ContDiffMapSupportedIn.coe_sub

deleted theorem ContDiffMapSupportedIn.coe_zero