Commit 2024-04-26 19:07 c4c2f8d6

View on Github →

chore: move LinearMap.range into its own file (#12378)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Exact.lean

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

added theorem AddMonoidHom.coe_toIntLinearMap_range

added theorem LinearMap.comap_injective

added theorem LinearMap.comap_le_comap_iff

added def LinearMap.iterateRange

added theorem LinearMap.ker_eq_bot_of_cancel

added theorem LinearMap.ker_le_iff

added theorem LinearMap.ker_rangeRestrict

added theorem LinearMap.map_le_range

added theorem LinearMap.mem_range

added theorem LinearMap.mem_range_self

added theorem LinearMap.mem_submoduleImage

added theorem LinearMap.mem_submoduleImage_of_le

added def LinearMap.range

added def LinearMap.rangeRestrict

added theorem LinearMap.range_codRestrict

added theorem LinearMap.range_coe

added theorem LinearMap.range_comp

added theorem LinearMap.range_comp_le_range

added theorem LinearMap.range_comp_of_range_eq_top

added theorem LinearMap.range_domRestrict_le_range

added theorem LinearMap.range_eq_bot

added theorem LinearMap.range_eq_map

added theorem LinearMap.range_eq_top

added theorem LinearMap.range_id

added theorem LinearMap.range_le_bot_iff

added theorem LinearMap.range_le_iff_comap

added theorem LinearMap.range_le_ker_iff

added theorem LinearMap.range_neg

added theorem LinearMap.range_rangeRestrict

added theorem LinearMap.range_smul'

added theorem LinearMap.range_smul

added theorem LinearMap.range_toAddSubgroup

added theorem LinearMap.range_toAddSubmonoid

added theorem LinearMap.range_zero

added def LinearMap.submoduleImage

added theorem LinearMap.submoduleImage_apply_of_le

added theorem LinearMap.surjective_rangeRestrict

added def Submodule.MapSubtype.orderEmbedding

added def Submodule.MapSubtype.relIso

added theorem Submodule.comap_subtype_eq_top

added theorem Submodule.comap_subtype_self

added theorem Submodule.map_comap_eq

added theorem Submodule.map_comap_eq_of_le

added theorem Submodule.map_comap_eq_self

added theorem Submodule.map_subtype_embedding_eq

added theorem Submodule.map_subtype_le

added theorem Submodule.map_subtype_range_inclusion

added theorem Submodule.map_subtype_top

added theorem Submodule.map_top

added theorem Submodule.range_inclusion

added theorem Submodule.range_subtype

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem AddMonoidHom.coe_toIntLinearMap_range

deleted theorem LinearMap.comap_injective

deleted theorem LinearMap.comap_le_comap_iff

deleted def LinearMap.iterateRange

deleted theorem LinearMap.ker_eq_bot_of_cancel

deleted theorem LinearMap.ker_le_iff

deleted theorem LinearMap.ker_rangeRestrict

deleted theorem LinearMap.map_le_range

deleted theorem LinearMap.mem_range

deleted theorem LinearMap.mem_range_self

deleted theorem LinearMap.mem_submoduleImage

deleted theorem LinearMap.mem_submoduleImage_of_le

deleted def LinearMap.range

deleted def LinearMap.rangeRestrict

deleted theorem LinearMap.range_codRestrict

deleted theorem LinearMap.range_coe

deleted theorem LinearMap.range_comp

deleted theorem LinearMap.range_comp_le_range

deleted theorem LinearMap.range_comp_of_range_eq_top

deleted theorem LinearMap.range_domRestrict_le_range

deleted theorem LinearMap.range_eq_bot

deleted theorem LinearMap.range_eq_map

deleted theorem LinearMap.range_eq_top

deleted theorem LinearMap.range_id

deleted theorem LinearMap.range_le_bot_iff

deleted theorem LinearMap.range_le_iff_comap

deleted theorem LinearMap.range_le_ker_iff

deleted theorem LinearMap.range_neg

deleted theorem LinearMap.range_rangeRestrict

deleted theorem LinearMap.range_smul'

deleted theorem LinearMap.range_smul

deleted theorem LinearMap.range_toAddSubgroup

deleted theorem LinearMap.range_toAddSubmonoid

deleted theorem LinearMap.range_zero

deleted def LinearMap.submoduleImage

deleted theorem LinearMap.submoduleImage_apply_of_le

deleted theorem LinearMap.surjective_rangeRestrict

deleted def Submodule.MapSubtype.orderEmbedding

deleted def Submodule.MapSubtype.relIso

deleted theorem Submodule.comap_subtype_eq_top

deleted theorem Submodule.comap_subtype_self

deleted theorem Submodule.map_comap_eq

deleted theorem Submodule.map_comap_eq_of_le

deleted theorem Submodule.map_comap_eq_self

deleted theorem Submodule.map_subtype_embedding_eq

deleted theorem Submodule.map_subtype_le

deleted theorem Submodule.map_subtype_range_inclusion

deleted theorem Submodule.map_subtype_top

deleted theorem Submodule.map_top

deleted theorem Submodule.range_inclusion

deleted theorem Submodule.range_subtype