Commit 2026-05-15 23:42 20ba84f1

View on Github →

feat: ContinuousLinearMap.restrict (#39344)

Estimated changes

Modified Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

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

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

added theorem LinearMap.coe_restrict_apply

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

added theorem LinearMap.comap_domRestrict

added theorem LinearMap.comap_restrict

added theorem LinearMap.map_domRestrict

added theorem LinearMap.map_restrict

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

modified theorem LinearMap.ker_rangeRestrict

added theorem LinearMap.range_restrict

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean

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

added theorem ContinuousLinearMap.coe_domRestrict

modified theorem ContinuousLinearMap.coe_projKerOfRightInverse_apply

added theorem ContinuousLinearMap.coe_restrict_apply

added def ContinuousLinearMap.domRestrict

added theorem ContinuousLinearMap.domRestrict_comp_codRestrict

modified def ContinuousLinearMap.projKerOfRightInverse

modified theorem ContinuousLinearMap.projKerOfRightInverse_apply_idem

modified theorem ContinuousLinearMap.projKerOfRightInverse_comp_inv

added def ContinuousLinearMap.restrict

added theorem ContinuousLinearMap.restrict_apply

added theorem ContinuousLinearMap.restrict_comp

added theorem ContinuousLinearMap.restrict_eq_codRestrict_domRestrict

added theorem ContinuousLinearMap.restrict_eq_domRestrict_codRestrict

added theorem ContinuousLinearMap.subtypeL_comp_restrict

added theorem ContinuousLinearMap.toLinearMap_codRestrict

added theorem ContinuousLinearMap.toLinearMap_domRestrict

added theorem ContinuousLinearMap.toLinearMap_rangeRestrict

added theorem ContinuousLinearMap.toLinearMap_restrict