Theorem LinearMap.surjective_comp_subtype_of_isComplemented

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_subtype_of_isComplementedView on Github →