Theorem Submodule.sub_projection_mem

Modification history

2026-05-11 15:25

Mathlib/LinearAlgebra/Projection.lean

refactor(LinearAlgebra/Projection): refactor `quotientEquivOfIsCompl` via `LinearEquiv.ofLinear` (#38814) …

Added Submodule.sub_projection_mem View on Github →