Theorem ContinuousLinearEquiv.toLinearquiv_ofIsHomeomorph

Modification history

2026-08-13 20:38
Mathlib/Topology/Algebra/Module/Equiv.lean
chore: split `ContinuousLinearMap.IsInvertible` to its own file (#42697) …
Deleted ContinuousLinearEquiv.toLinearquiv_ofIsHomeomorphView on Github →
2026-06-24 17:13
Mathlib/Topology/Algebra/Module/Equiv.lean
feat(Mathlib.Topology.Algebra.Module.Equiv): add results on IsHomeomorph (#39476) …
Added ContinuousLinearEquiv.toLinearquiv_ofIsHomeomorphView on Github →