Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-05 12:11 70269f3c

View on Github →

feat(order/*): introduces complemented lattices (#5747) Defines is_complemented on bounded lattices Proves facts about complemented modular lattices Provides two instances of is_complemented on submodule lattices

Estimated changes

Modified src/linear_algebra/basis.lean

Modified src/order/atoms.lean

added theorem is_atomic_iff_is_coatomic

added theorem is_atomic_of_is_coatomic_of_is_complemented_of_is_modular

added theorem is_coatomic_of_is_atomic_of_is_complemented_of_is_modular

Modified src/order/boolean_algebra.lean

Modified src/order/bounded_lattice.lean

added theorem eq_bot_of_is_compl_top

added theorem eq_bot_of_top_is_compl

added theorem eq_top_of_bot_is_compl

added theorem eq_top_of_is_compl_bot

Modified src/order/modular_lattice.lean

Modified src/representation_theory/maschke.lean

modified theorem monoid_algebra.exists_left_inverse_of_injective

modified theorem monoid_algebra.submodule.exists_is_compl

added theorem monoid_algebra.submodule.is_complemented