Theorem ContinuousLinearMap.IsInvertible.inverse_apply_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_apply_selfView on Github →
2026-01-04 16:08
Mathlib/Topology/Algebra/Module/Equiv.lean
feat(Topology/Algebra/Module/Equiv): add 2 lemmas (#33510)
Added ContinuousLinearMap.IsInvertible.inverse_apply_selfView on Github →