Theorem ContinuousLinearMap.toLinearMap_pow

Modification history

2026-07-27 16:25
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
chore(Data/FunLike): tag `IsApply` lemmas as simp (#42027) …
Added ContinuousLinearMap.toLinearMap_powView on Github →