Theorem Submodule.toLinearMap_quotientEquivOfIsCompl

Modification history

2026-05-11 15:25

Mathlib/LinearAlgebra/Projection.lean

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

Added Submodule.toLinearMap_quotientEquivOfIsCompl View on Github →