Commit 2024-11-04 18:22 8c245d44

View on Github →

feat: introduce ContinuousLinearMap.IsInvertible and basic API (#18402) To be used when defining the pullback of vector fields in #18396

Estimated changes

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

added def ContinuousLinearEquiv.equivOfInverse'

added theorem ContinuousLinearEquiv.equivOfInverse'_apply

added theorem ContinuousLinearEquiv.symm_equivOfInverse'

added theorem ContinuousLinearMap.IsInvertible.comp

added theorem ContinuousLinearMap.IsInvertible.inverse_apply_eq

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.of_inverse

added def ContinuousLinearMap.IsInvertible

added theorem ContinuousLinearMap.inverse_comp_equiv

added theorem ContinuousLinearMap.inverse_eq

added theorem ContinuousLinearMap.inverse_equiv_comp

added theorem ContinuousLinearMap.inverse_id

deleted theorem ContinuousLinearMap.inverse_non_equiv

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