Mathlib Changelog
v4
Changelog
About
Github
Theorem
Disjoint.isCompl_sup_right_of_isCompl_sup_left
Modification history
2023-10-07 06:50
Mathlib/Order/ModularLattice.lean
chore: relax typeclass assumptions in two modular lattice lemmas (#7555)
Modified
Disjoint.isCompl_sup_right_of_isCompl_sup_left
View on Github →
2023-10-06 12:22
Mathlib/Order/ModularLattice.lean
feat: add lemmas `Disjoint.isCompl_sup_right_of_isCompl_sup_left` (and partner) (#7483)
Added
Disjoint.isCompl_sup_right_of_isCompl_sup_left
View on Github →