Theorem LocallyConstant.coe_smul

Modification history

2026-09-18 15:04
Mathlib/Topology/LocallyConstant/Algebra.lean
chore: catch up on a lot of `to_additive` debt (#43814) …
Deleted LocallyConstant.coe_smulView on Github →
2023-03-03 19:32
Mathlib/Topology/LocallyConstant/Algebra.lean
feat: port Topology.LocallyConstant.Algebra (#2592)
Added LocallyConstant.coe_smulView on Github →