Theorem LinearMap.pi_proj

Modification history

2026-10-27 00:37
Mathlib/Algebra/Module/Pi.lean
chore(Algebra): move `LinearMap.proj` and `LinearMap.pi` (#45302) …
Modified LinearMap.pi_projView on Github →
2025-02-24 08:51
Mathlib/LinearAlgebra/Pi.lean
feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162)
Added LinearMap.pi_projView on Github →