Commit 2023-01-28 21:17 51f3caa8

View on Github →

feat: port Algebra.Module.Submodule.Lattice (#1898)

Estimated changes

Modified Mathlib.lean

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

added theorem AddSubgroup.coe_toIntSubmodule

added def AddSubgroup.toIntSubmodule

added theorem AddSubgroup.toIntSubmodule_symm

added theorem AddSubgroup.toIntSubmodule_toAddSubgroup

added theorem AddSubmonoid.coe_toNatSubmodule

added def AddSubmonoid.toNatSubmodule

added theorem AddSubmonoid.toNatSubmodule_symm

added theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid

added theorem Submodule.add_mem_sup

added def Submodule.botEquivPUnit

added theorem Submodule.bot_coe

added theorem Submodule.bot_toAddSubmonoid

added theorem Submodule.disjoint_def'

added theorem Submodule.disjoint_def

added theorem Submodule.eq_bot_of_subsingleton

added theorem Submodule.eq_top_iff'

added theorem Submodule.eq_zero_of_coe_mem_of_disjoint

added theorem Submodule.exists_mem_ne_zero_of_ne_bot

added theorem Submodule.finset_inf_coe

added theorem Submodule.inf_coe

added theorem Submodule.infᵢ_coe

added theorem Submodule.infₛ_coe

added theorem Submodule.mem_bot

added theorem Submodule.mem_finset_inf

added theorem Submodule.mem_inf

added theorem Submodule.mem_infᵢ

added theorem Submodule.mem_infₛ

added theorem Submodule.mem_sup_left

added theorem Submodule.mem_sup_right

added theorem Submodule.mem_supᵢ_of_mem

added theorem Submodule.mem_supₛ_of_mem

added theorem Submodule.mem_top

added theorem Submodule.nonzero_mem_of_bot_lt

added theorem Submodule.restrictScalars_bot

added theorem Submodule.restrictScalars_eq_bot_iff

added theorem Submodule.restrictScalars_eq_top_iff

added theorem Submodule.restrictScalars_top

added theorem Submodule.sub_mem_sup

added theorem Submodule.sum_mem_bsupr

added theorem Submodule.sum_mem_supᵢ

added theorem Submodule.toAddSubgroup_toIntSubmodule

added theorem Submodule.toAddSubmonoid_toNatSubmodule

added def Submodule.topEquiv

added theorem Submodule.top_coe

added theorem Submodule.top_toAddSubmonoid