Theorem LinearMap.proj_pi

Modification history

2025-02-24 08:51

Mathlib/LinearAlgebra/Pi.lean

feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162)

Modified LinearMap.proj_pi View on Github →

2023-02-14 06:34

Mathlib/LinearAlgebra/Pi.lean

feat: port LinearAlgebra.Pi (#2250)

Added LinearMap.proj_pi View on Github →