Commit 2026-05-14 02:11 7e71961a

View on Github →

feat: semilinearize LinearMap.restrict (#39335)

Estimated changes

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

modified def LinearMap.restrict

modified theorem LinearMap.restrict_apply

modified theorem LinearMap.restrict_coe_apply

modified theorem LinearMap.restrict_comp

modified theorem LinearMap.restrict_eq_codRestrict_domRestrict

modified theorem LinearMap.restrict_eq_domRestrict_codRestrict

modified theorem LinearMap.restrict_sub

modified theorem LinearMap.subtype_comp_restrict