Theorem ContinuousLinearMap.pi_proj_comp

Modification history

2025-02-24 08:51
Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162)
Added ContinuousLinearMap.pi_proj_compView on Github →