Theorem Submodule.quotientEquivOfIsCompl_apply_mk

Modification history

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