Theorem Submodule.continuous_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.continuous_mkQView on Github →