Theorem Submodule.range_projectionOntoL

Modification history

2026-05-05 16:21

Mathlib/Topology/Algebra/Module/Complement.lean

chore(LinearAlgebra/Projection): rename `Submodule.linearProjOfIsCompl` to `Submodule.projectionOnto` (#38956) …

Modified Submodule.range_projectionOntoL View on Github →

2026-05-05 09:37

Mathlib/Topology/Algebra/Module/Complement.lean

feat: define Submodule.IsTopCompl (#38547) …

Added Submodule.range_projectionOntoL View on Github →