Commit 2026-03-03 16:04 89898ca8
View on Github →refactor(Topology/Algebra/Module/LinearMap): adjust statement of coe_mul and coe_pow (#35269)
In Topology/Algebra/Module/LinearMap, it seems to be the pattern to have coe_zero/coe_id/coe_add/coe_neg/coe_sub for the coercions from ContinuousLinearMap to LinearMap and primed versions coe_zero'/coe_id'/coe_add'/coe_neg'/coe_sub' for the coercions from ContinuousLinearMap to Function.
This PR adjusts the statements of coe_mul and coe_pow to fit this pattern, as well as adding coe_one.