Commit 2026-08-23 12:41 d606315d

View on Github →

feat: a continuous linear map is invertible iff it is an homeomorphism (#42698) Also a bit of cleanup in the file.

Estimated changes

Modified Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Invertible.lean

added theorem ContinuousLinearMap.isInvertible_iff_isHomeomorph

modified theorem ContinuousLinearMap.isInvertible_inverse_iff

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added theorem ContinuousLinearEquiv.toContinuousLinearMap_equivOfInverse'

added theorem ContinuousLinearEquiv.toContinuousLinearMap_equivOfInverse