Commit 2026-10-29 22:29 7881f45c

View on Github →

chore(Topology): use IsApply for ContinuousMapZero (#45292)

Estimated changes

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

deleted theorem ContinuousMapZero.coe_add

deleted theorem ContinuousMapZero.coe_mul

deleted theorem ContinuousMapZero.coe_neg

deleted theorem ContinuousMapZero.coe_smul

deleted theorem ContinuousMapZero.coe_sub

modified theorem ContinuousMapZero.coe_sum

deleted theorem ContinuousMapZero.coe_zero