Theorem ContinuousLinearMap.isIdempotentElem_toLinearMap_iff

Modification history

2026-05-20 20:03

Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean

chore: split Topology.Algebra.Module.LinearMap (#39612) …

Modified ContinuousLinearMap.isIdempotentElem_toLinearMap_iff View on Github →

2025-08-04 22:28

Mathlib/Topology/Algebra/Module/LinearMap.lean

feat(Topology/Algebra/Module/LinearMap): add `ContinuousLinearMap.isIdempotentElem_toLinearMap_iff` (#27942) …

Added ContinuousLinearMap.isIdempotentElem_toLinearMap_iff View on Github →