Commit 2025-08-04 22:28 5e6c9d1d
View on Github →feat(Topology/Algebra/Module/LinearMap): add ContinuousLinearMap.isIdempotentElem_toLinearMap_iff (#27942)
Instead of having to annoyingly do congr(LinearMapClass.linearMap $h.eq) over and over to use results for idempotent linear maps, we can just do h.toLinearMap, where h : IsIdempotentElem T for some continuous linear map T.