Theorem ContinuousLinearMap.coe_pow'

Modification history

2026-07-27 16:25
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
chore(Data/FunLike): tag `IsApply` lemmas as simp (#42027) …
Deleted ContinuousLinearMap.coe_pow'View on Github →
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_pow'View on Github →