Theorem Submodule.toLinearMap_symm_quotientEquivOfIsCompl

Modification history

2026-05-11 15:25
Mathlib/LinearAlgebra/Projection.lean
refactor(LinearAlgebra/Projection): refactor `quotientEquivOfIsCompl` via `LinearEquiv.ofLinear` (#38814) …
Added Submodule.toLinearMap_symm_quotientEquivOfIsComplView on Github →