Theorem ContinuousLinearMap.coe_one

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_one View on Github →