Theorem Submodule.isQuotientMap_mkQ

Modification history

2026-05-04 13:04
Mathlib/Topology/Algebra/Module/Basic.lean
feat(Topology/Algebra/Module): bundle Submodule.mkQ as a continuous linear map (#38811) …
Added Submodule.isQuotientMap_mkQView on Github →