Theorem ContinuousLinearEquiv.submoduleMap_symm_apply

Modification history

2025-12-27 09:40
Mathlib/Topology/Algebra/Module/Equiv.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified ContinuousLinearEquiv.submoduleMap_symm_applyView on Github →
2025-11-21 15:41
Mathlib/Topology/Algebra/Module/Equiv.lean
feat: ContinuousLinearEquiv.submoduleMap and friends (#31899) …
Added ContinuousLinearEquiv.submoduleMap_symm_applyView on Github →