Commit 2026-09-29 22:08 b5b68124

View on Github →

feat: generalize SMul instances from DistribMulAction to DistribSMul (#41736) or similar (SMulWithZero -> SMulZeroClass)

Estimated changes

Modified Mathlib/Algebra/Lie/Free.lean

modified theorem FreeLieAlgebra.Rel.smulOfTower

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

Modified Mathlib/Geometry/Convex/AffineMap/Module.lean

Modified Mathlib/Geometry/Convex/ConvexSpace/Module.lean

Modified Mathlib/RepresentationTheory/Continuous/Basic.lean

Modified Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean

Modified Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

modified theorem ZeroAtInftyContinuousMap.coe_smul

modified theorem ZeroAtInftyContinuousMap.smul_apply

Modified Mathlib/Topology/ContinuousMap/ZeroAtInftyUnitization.lean

modified theorem ZeroAtInftyContinuousMap.toOnePoint_smul