Theorem Submodule.linearProjOfIsCompl_surjective

Modification history

2025-05-01 06:42
Mathlib/LinearAlgebra/Projection.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added Submodule.linearProjOfIsCompl_surjectiveView on Github →