Commit 2026-06-25 09:00 22a6ad55

View on Github →

feat: define LinearMap.IsQuasiInverse (#39475) If the name "QuasiInverse" is considered too vague, I am open to suggestions. This was written by @PatrickMassot and @CoolRmal at the May 2026 ICERM workshop as part of the project on Fredholm operators.

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/FiniteRange.lean

modified def LinearMap.HasFiniteRange

modified def LinearMap.HasNoetherianRange

added theorem LinearMap.IsLeftQuasiInverse.comp

added theorem LinearMap.IsLeftQuasiInverse.congr

added theorem LinearMap.IsLeftQuasiInverse.equiv

added theorem LinearMap.IsLeftQuasiInverse.of_comp_left

added def LinearMap.IsLeftQuasiInverse

added theorem LinearMap.IsQuasiInverse.comp

added theorem LinearMap.IsQuasiInverse.congr

added theorem LinearMap.IsQuasiInverse.equiv_of_left

added theorem LinearMap.IsQuasiInverse.equiv_of_right

added theorem LinearMap.IsQuasiInverse.of_comp_left

added theorem LinearMap.IsQuasiInverse.of_comp_right

added theorem LinearMap.IsQuasiInverse.symm

added def LinearMap.IsQuasiInverse

added theorem LinearMap.IsRightQuasiInverse.comp

added theorem LinearMap.IsRightQuasiInverse.congr

added theorem LinearMap.IsRightQuasiInverse.equiv

added theorem LinearMap.IsRightQuasiInverse.of_comp_right

added def LinearMap.IsRightQuasiInverse

added theorem LinearMap.isLeftQuasiInverse_congr

added theorem LinearMap.isLeftQuasiInverse_iff_isRightQuasiInverse_swap

added theorem LinearMap.isQuasiInverse_congr

added theorem LinearMap.isRightQuasiInverse_congr