Theorem LinearMap.surjective_comp_linearProjOfIsCompl

Modification history

2025-09-04 11:48
Mathlib/LinearAlgebra/Projection.lean
feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End` (#24015)
Added LinearMap.surjective_comp_linearProjOfIsComplView on Github →