Theorem ContinuousLinearMap.IsInvertible.inverse_comp_self

Modification history

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_comp_selfView 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_comp_selfView on Github →