Commit 2025-03-18 23:33 c840e23c

View on Github →

chore: use to_additive for bounded continuous functions (#23013)

Estimated changes

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

deleted theorem BoundedContinuousFunction.add_apply

deleted theorem BoundedContinuousFunction.coe_add

deleted theorem BoundedContinuousFunction.coe_nsmul

modified theorem BoundedContinuousFunction.coe_nsmulRec

deleted theorem BoundedContinuousFunction.nsmul_apply