Theorem ContinuousLinearMap.isInvertible_inverse_iff

Modification history

2026-08-23 12:41
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Invertible.lean
feat: a continuous linear map is invertible iff it is an homeomorphism (#42698) …
Modified ContinuousLinearMap.isInvertible_inverse_iffView on Github →
2026-08-13 20:38
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Invertible.lean
chore: split `ContinuousLinearMap.IsInvertible` to its own file (#42697) …
Modified ContinuousLinearMap.isInvertible_inverse_iffView on Github →
2025-12-20 01:04
Mathlib/Topology/Algebra/Module/Equiv.lean
feat(Topology/Algebra/Module): lemmas about `IsInvertible` (#33027) …
Added ContinuousLinearMap.isInvertible_inverse_iffView on Github →