Commit 2026-05-11 15:25 229580e5

View on Github →

refactor(LinearAlgebra/Projection): refactor quotientEquivOfIsCompl via LinearEquiv.ofLinear (#38814) This PR refactors Submodule.quotientEquivOfIsCompl to use LinearEquiv.ofLinear rather than LinearEquiv.symm <| LinearEquiv.ofBijective. The new definition makes both directions of the equivalence explicit: the forward idirection is Submodule.liftQ of the projection onto q along p, and the backward direction is Submodule.mkQ composed with the inclusion q in E.

Estimated changes

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem Submodule.quotientEquivOfIsCompl_apply_mk

deleted theorem Submodule.quotientEquivOfIsCompl_apply_mk_coe

added theorem Submodule.quotientEquivOfIsCompl_apply_mk_right

deleted theorem Submodule.quotientEquivOfIsCompl_symm_apply

added theorem Submodule.sub_projection_mem

added theorem Submodule.toLinearMap_quotientEquivOfIsCompl

added theorem Submodule.toLinearMap_symm_quotientEquivOfIsCompl