Theorem LinearMap.proj_surjective

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_surjectiveView on Github →
2025-02-07 18:54
Mathlib/LinearAlgebra/Pi.lean
feat: Prerequisites for Hopkins–Levitzki theorem (#21544) …
Added LinearMap.proj_surjectiveView on Github →