Commit 2025-12-20 01:04 9a32d095

View on Github →

feat(Topology/Algebra/Module): lemmas about IsInvertible (#33027) From https://github.com/urkud/SardMoreira

Estimated changes

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

added theorem ContinuousLinearMap.IsInvertible.inverse_comp_self

added theorem ContinuousLinearMap.IsInvertible.self_comp_inverse

added theorem ContinuousLinearMap.isInvertible_inverse_iff