Commit 2025-10-30 18:35 82dd7918

View on Github →

feat(BoundedContinuousFunction): multiplicative versions (#31089) Provide multiplicative versions for BoundedContinuousFunction.coeFnAddHom and similar. They were only defined for the additive case.

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

deleted def BoundedContinuousFunction.coeFnAddHom

added def BoundedContinuousFunction.coeFnMonoidHom

added theorem BoundedContinuousFunction.coe_prod

deleted theorem BoundedContinuousFunction.coe_sum

added theorem BoundedContinuousFunction.prod_apply

deleted theorem BoundedContinuousFunction.sum_apply

deleted def BoundedContinuousFunction.toContinuousMapAddHom

added def BoundedContinuousFunction.toContinuousMapMonoidHom

Modified Mathlib/Topology/ContinuousMap/Compact.lean