Theorem LinearMap.ofIsCompl_right_apply

Modification history

2026-05-19 15:28
Mathlib/LinearAlgebra/Projection.lean
feat(Topology/Algebra/Module/Complement): bundle `prodEquivOfIsCompl` and `quotientEquivOfIsCompl`, add `ContinuousLinearMap.ofIsTopCompl` (#39260) …
Deleted LinearMap.ofIsCompl_right_applyView on Github →
2023-02-22 13:01
Mathlib/LinearAlgebra/Projection.lean
feat: port LinearAlgebra.Projection (#2431)
Added LinearMap.ofIsCompl_right_applyView on Github →