Commit 2026-08-13 20:38 e310d5e0

View on Github →

chore: split ContinuousLinearMap.IsInvertible to its own file (#42697) The original file is getting way too big, and this makes complete sense as an independent file imo.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Const.lean

Modified Mathlib/Analysis/Normed/Module/ContinuousInverse.lean

Modified Mathlib/Analysis/Normed/Operator/Fredholm/Basic.lean

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

added theorem ContinuousLinearMap.IsInvertible.comp

added theorem ContinuousLinearMap.IsInvertible.inverse_apply_eq

added theorem ContinuousLinearMap.IsInvertible.inverse_apply_self

added theorem ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_left

added theorem ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right

added theorem ContinuousLinearMap.IsInvertible.inverse_comp_of_left

added theorem ContinuousLinearMap.IsInvertible.inverse_comp_of_right

added theorem ContinuousLinearMap.IsInvertible.inverse_comp_self

added theorem ContinuousLinearMap.IsInvertible.of_inverse

added theorem ContinuousLinearMap.IsInvertible.self_apply_inverse

added theorem ContinuousLinearMap.IsInvertible.self_comp_inverse

added def ContinuousLinearMap.IsInvertible

added theorem ContinuousLinearMap.inverse_comp_equiv

added theorem ContinuousLinearMap.inverse_eq

added theorem ContinuousLinearMap.inverse_eq_ringInverse

added theorem ContinuousLinearMap.inverse_equiv

added theorem ContinuousLinearMap.inverse_equiv_comp

added theorem ContinuousLinearMap.inverse_id

added theorem ContinuousLinearMap.inverse_of_not_isInvertible

added theorem ContinuousLinearMap.inverse_zero

added theorem ContinuousLinearMap.isInvertible_comp_equiv

added theorem ContinuousLinearMap.isInvertible_equiv

added theorem ContinuousLinearMap.isInvertible_equiv_comp

added theorem ContinuousLinearMap.isInvertible_inverse_iff

added theorem ContinuousLinearMap.isInvertible_zero_iff

added theorem ContinuousLinearMap.ringInverse_eq_inverse

added theorem ContinuousLinearMap.ringInverse_equiv

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

added theorem ContinuousLinearEquiv.toLinearEquiv_ofIsHomeomorph

deleted theorem ContinuousLinearEquiv.toLinearquiv_ofIsHomeomorph

deleted theorem ContinuousLinearMap.IsInvertible.comp

deleted theorem ContinuousLinearMap.IsInvertible.inverse_apply_eq

deleted theorem ContinuousLinearMap.IsInvertible.inverse_apply_self

deleted theorem ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_left

deleted theorem ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right

deleted theorem ContinuousLinearMap.IsInvertible.inverse_comp_of_left

deleted theorem ContinuousLinearMap.IsInvertible.inverse_comp_of_right

deleted theorem ContinuousLinearMap.IsInvertible.inverse_comp_self

deleted theorem ContinuousLinearMap.IsInvertible.of_inverse

deleted theorem ContinuousLinearMap.IsInvertible.self_apply_inverse

deleted theorem ContinuousLinearMap.IsInvertible.self_comp_inverse

deleted def ContinuousLinearMap.IsInvertible

modified theorem ContinuousLinearMap.coprod_comp_prodComm

deleted theorem ContinuousLinearMap.inverse_comp_equiv

deleted theorem ContinuousLinearMap.inverse_eq

deleted theorem ContinuousLinearMap.inverse_eq_ringInverse

deleted theorem ContinuousLinearMap.inverse_equiv

deleted theorem ContinuousLinearMap.inverse_equiv_comp

deleted theorem ContinuousLinearMap.inverse_id

deleted theorem ContinuousLinearMap.inverse_of_not_isInvertible

deleted theorem ContinuousLinearMap.inverse_zero

deleted theorem ContinuousLinearMap.isInvertible_comp_equiv

deleted theorem ContinuousLinearMap.isInvertible_equiv

deleted theorem ContinuousLinearMap.isInvertible_equiv_comp

deleted theorem ContinuousLinearMap.isInvertible_inverse_iff

deleted theorem ContinuousLinearMap.isInvertible_zero_iff

deleted theorem ContinuousLinearMap.ringInverse_eq_inverse

deleted theorem ContinuousLinearMap.ringInverse_equiv