Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-19 14:35 591c34b6

View on Github →

refactor(linear_algebra/basic): move the lattice structure to its own file (#6767) The entire lattice structure is thoroughly uninteresting. By moving it to its own shorter file, it should be easier to unify with the lattice of submonoid I'd hope in future we can generate this automatically for any subobject A with an injection into set A.

Estimated changes

added theorem submodule.Inf_coe
added theorem submodule.bot_coe
added theorem submodule.eq_top_iff'
added theorem submodule.exists_of_lt
added theorem submodule.inf_coe
added theorem submodule.infi_coe
added theorem submodule.le_def'
added theorem submodule.le_def
added theorem submodule.lt_def
added theorem submodule.mem_Inf
added theorem submodule.mem_bot
added theorem submodule.mem_inf
added theorem submodule.mem_infi
added theorem submodule.mem_sup_left
added theorem submodule.mem_top
added theorem submodule.top_coe
deleted theorem submodule.Inf_coe
deleted theorem submodule.bot_coe
deleted theorem submodule.coe_subset_coe
deleted theorem submodule.eq_top_iff'
deleted theorem submodule.exists_of_lt
deleted theorem submodule.inf_coe
deleted theorem submodule.infi_coe
deleted theorem submodule.le_def'
deleted theorem submodule.le_def
deleted theorem submodule.lt_def
deleted theorem submodule.mem_Inf
deleted theorem submodule.mem_Sup_of_mem
deleted theorem submodule.mem_bot
deleted theorem submodule.mem_inf
deleted theorem submodule.mem_infi
deleted theorem submodule.mem_sup_left
deleted theorem submodule.mem_sup_right
deleted theorem submodule.mem_supr_of_mem
deleted theorem submodule.mem_top
deleted theorem submodule.top_coe