Theorem ContinuousLinearMap.coe_mul'

Modification history

2026-03-03 16:04
Mathlib/Topology/Algebra/Module/LinearMap.lean
refactor(Topology/Algebra/Module/LinearMap): adjust statement of `coe_mul` and `coe_pow` (#35269) …
Added ContinuousLinearMap.coe_mul'View on Github →