[Merged by Bors] - feat: ContinuousLinearEquiv.submoduleMap and friends - #31899

Closed

grunweg wants to merge 9 commits into

leanprover-community:masterfrom

grunweg:cle-submodulemap

Commits on Nov 21, 2025

feat: ContinuousLinearEquiv.submoduleMap
grunweg
committed
ad31c96
Also define ofSubmodules and submoduleMap'
grunweg
committed
48b1009
Re-order: variable management is slightly annoying
grunweg
committed
a0e4b29
Sorry-free: need to move the homeomorphism lemma
grunweg
committed
d88977f
Move lemmas
grunweg
committed
25eedf0
Better name
grunweg
committed
c0307c4
Review comments
grunweg
committed
2c4a986
Style tweaks
grunweg
committed
158bad5
More docs
grunweg
committed
06f985d