Commit 2023-10-26 10:03 49f7f62d

View on Github →

chore: move Submodule.{map,comap} to Algebra.Module.Submodule.Map (#7925)

Estimated changes

Modified Mathlib.lean

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

added theorem AddMonoidHom.coe_toIntLinearMap_map

added theorem AddMonoidHom.coe_toMultiplicative_map

added theorem LinearMap.iInf_invariant

added theorem MonoidHom.coe_toAdditive_map

added theorem Submodule.AddMonoidHom.coe_toIntLinearMap_comap

added theorem Submodule.apply_coe_mem_map

added theorem Submodule.coe_equivMapOfInjective_apply

added def Submodule.comap

added def Submodule.comapSubtypeEquivOfLe

added theorem Submodule.comapSubtypeEquivOfLe_apply_coe

added theorem Submodule.comap_coe

added theorem Submodule.comap_comp

added theorem Submodule.comap_equiv_eq_map_symm

added theorem Submodule.comap_iInf

added theorem Submodule.comap_iInf_map_of_injective

added theorem Submodule.comap_iSup_map_of_injective

added theorem Submodule.comap_id

added theorem Submodule.comap_inf

added theorem Submodule.comap_inf_map_of_injective

added theorem Submodule.comap_injective_of_surjective

added theorem Submodule.comap_le_comap_iff_of_surjective

added theorem Submodule.comap_le_comap_smul

added theorem Submodule.comap_map_eq_of_injective

added theorem Submodule.comap_mono

added theorem Submodule.comap_smul'

added theorem Submodule.comap_smul

added theorem Submodule.comap_strictMono_of_surjective

added theorem Submodule.comap_sup_map_of_injective

added theorem Submodule.comap_surjective_of_injective

added theorem Submodule.comap_top

added theorem Submodule.comap_zero

added def Submodule.compatibleMaps

added theorem Submodule.eq_zero_of_bot_submodule

added theorem Submodule.gc_map_comap

added def Submodule.gciMapComap

added def Submodule.giMapComap

added theorem Submodule.inf_comap_le_comap_add

added theorem Submodule.le_comap_map

added theorem Submodule.le_comap_pow_of_le_comap

added def Submodule.map

added theorem Submodule.map_add_le

added theorem Submodule.map_bot

added theorem Submodule.map_coe

added theorem Submodule.map_comap_eq_of_surjective

added theorem Submodule.map_comap_le

added theorem Submodule.map_comap_subtype

added theorem Submodule.map_comp

added theorem Submodule.map_equiv_eq_comap_symm

added theorem Submodule.map_iInf_comap_of_surjective

added theorem Submodule.map_iSup

added theorem Submodule.map_iSup_comap_of_sujective

added theorem Submodule.map_id

added theorem Submodule.map_inf

added theorem Submodule.map_inf_comap_of_surjective

added theorem Submodule.map_inf_eq_map_inf_comap

added theorem Submodule.map_inf_le

added theorem Submodule.map_injective_of_injective

added theorem Submodule.map_le_iff_le_comap

added theorem Submodule.map_le_map_iff_of_injective

added theorem Submodule.map_mono

added theorem Submodule.map_smul'

added theorem Submodule.map_strictMono_of_injective

added theorem Submodule.map_sup

added theorem Submodule.map_sup_comap_of_surjective

added theorem Submodule.map_surjective_of_surjective

added theorem Submodule.map_symm_eq_iff

added theorem Submodule.map_toAddSubmonoid'

added theorem Submodule.map_toAddSubmonoid

added theorem Submodule.map_zero

added theorem Submodule.mem_comap

added theorem Submodule.mem_map

added theorem Submodule.mem_map_equiv

added theorem Submodule.mem_map_of_mem

added def Submodule.orderIsoMapComap

added theorem Submodule.orderIsoMapComap_apply'

added theorem Submodule.orderIsoMapComap_symm_apply'

added theorem Submodule.range_map_nonempty

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem AddMonoidHom.coe_toIntLinearMap_map

deleted theorem AddMonoidHom.coe_toMultiplicative_map

deleted theorem LinearMap.iInf_invariant

deleted theorem MonoidHom.coe_toAdditive_map

deleted theorem Submodule.AddMonoidHom.coe_toIntLinearMap_comap

deleted theorem Submodule.apply_coe_mem_map

deleted theorem Submodule.coe_equivMapOfInjective_apply

deleted def Submodule.comap

deleted def Submodule.comapSubtypeEquivOfLe

deleted theorem Submodule.comapSubtypeEquivOfLe_apply_coe

deleted theorem Submodule.comap_coe

deleted theorem Submodule.comap_comp

deleted theorem Submodule.comap_equiv_eq_map_symm

deleted theorem Submodule.comap_iInf

deleted theorem Submodule.comap_iInf_map_of_injective

deleted theorem Submodule.comap_iSup_map_of_injective

deleted theorem Submodule.comap_id

deleted theorem Submodule.comap_inf

deleted theorem Submodule.comap_inf_map_of_injective

deleted theorem Submodule.comap_injective_of_surjective

deleted theorem Submodule.comap_le_comap_iff_of_surjective

deleted theorem Submodule.comap_le_comap_smul

deleted theorem Submodule.comap_map_eq_of_injective

deleted theorem Submodule.comap_mono

deleted theorem Submodule.comap_smul'

deleted theorem Submodule.comap_smul

deleted theorem Submodule.comap_strictMono_of_surjective

deleted theorem Submodule.comap_sup_map_of_injective

deleted theorem Submodule.comap_surjective_of_injective

deleted theorem Submodule.comap_top

deleted theorem Submodule.comap_zero

deleted def Submodule.compatibleMaps

deleted theorem Submodule.eq_zero_of_bot_submodule

deleted theorem Submodule.gc_map_comap

deleted def Submodule.gciMapComap

deleted def Submodule.giMapComap

deleted theorem Submodule.inf_comap_le_comap_add

deleted theorem Submodule.le_comap_map

deleted theorem Submodule.le_comap_pow_of_le_comap

deleted def Submodule.map

deleted theorem Submodule.map_add_le

deleted theorem Submodule.map_bot

deleted theorem Submodule.map_coe

deleted theorem Submodule.map_comap_eq_of_surjective

deleted theorem Submodule.map_comap_le

deleted theorem Submodule.map_comap_subtype

deleted theorem Submodule.map_comp

deleted theorem Submodule.map_equiv_eq_comap_symm

deleted theorem Submodule.map_iInf_comap_of_surjective

deleted theorem Submodule.map_iSup

deleted theorem Submodule.map_iSup_comap_of_sujective

deleted theorem Submodule.map_id

deleted theorem Submodule.map_inf

deleted theorem Submodule.map_inf_comap_of_surjective

deleted theorem Submodule.map_inf_eq_map_inf_comap

deleted theorem Submodule.map_inf_le

deleted theorem Submodule.map_injective_of_injective

deleted theorem Submodule.map_le_iff_le_comap

deleted theorem Submodule.map_le_map_iff_of_injective

deleted theorem Submodule.map_mono

deleted theorem Submodule.map_smul'

deleted theorem Submodule.map_strictMono_of_injective

deleted theorem Submodule.map_sup

deleted theorem Submodule.map_sup_comap_of_surjective

deleted theorem Submodule.map_surjective_of_surjective

deleted theorem Submodule.map_symm_eq_iff

deleted theorem Submodule.map_toAddSubmonoid'

deleted theorem Submodule.map_toAddSubmonoid

deleted theorem Submodule.map_zero

deleted theorem Submodule.mem_comap

deleted theorem Submodule.mem_map

deleted theorem Submodule.mem_map_equiv

deleted theorem Submodule.mem_map_of_mem

deleted def Submodule.orderIsoMapComap

deleted theorem Submodule.orderIsoMapComap_apply'

deleted theorem Submodule.orderIsoMapComap_symm_apply'

deleted theorem Submodule.range_map_nonempty