Commit 2026-07-02 16:39 e653de1e

View on Github →

chore: cleanup API around LinearMap.injective_domRestrict_iff (#41229)

Use Disjoint in LinearMap.injective_domRestrict_iff, and simplify the proof greatly.
Allow linear maps between two different spaces in LinearMap.injective_restrict_iff_disjoint, and rename it to LinearMap.injective_restrict_iff for consistency with the former
Add LinearMap.injective_codRestrict_iff for completeness

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Ker.lean

added theorem LinearMap.injective_codRestrict_iff

added theorem LinearMap.injective_restrict_iff

deleted theorem LinearMap.injective_restrict_iff_disjoint

Modified Mathlib/Data/Subtype.lean

added theorem Subtype.coind_injective_iff

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean

Modified Mathlib/RingTheory/Noetherian/Basic.lean