Commit 2026-07-01 17:54 b39dd4b5

View on Github →

chore: cleanup API around LinearMap.surjective_domRestrict_iff (#41235)

semilinearize LinearMap.range_domRestrict
add map_eq_range_iff as a replacement for LinearMap.range_domRestrict_eq_range_iff, with a golfed proof.
use Codisjoint in LinearMap.surjective_domRestrict_iff

Estimated changes

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

modified theorem LinearMap.range_domRestrict

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem Submodule.map_eq_range_iff

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