Commit 2021-01-22 12:52 de10203f

View on Github →

feat(order/modular_lattice): define modular lattices (#5564) Defines modular lattices Defines the diamond isomorphisms in a modular lattice Places is_modular_lattice instances on a distrib_lattice, the lattice of subgroups of a comm_group, and the lattice of submodules of a module.

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.mem_sup'

added theorem subgroup.mem_sup

Modified src/linear_algebra/basic.lean

Modified src/order/atoms.lean

added theorem is_compl.is_atom_iff_is_coatom

added theorem is_compl.is_coatom_iff_is_atom

Created src/order/modular_lattice.lean

added def inf_Icc_order_iso_Icc_sup

added theorem inf_sup_assoc_of_le

added def is_compl.Iic_order_iso_Ici

added theorem is_modular_lattice.sup_inf_sup_assoc

added theorem is_modular_lattice_iff_sup_inf_sup_assoc

added theorem sup_inf_assoc_of_le