Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-07 06:50
7732480f
View on Github →
chore: relax typeclass assumptions in two modular lattice lemmas (
#7555
)
Estimated changes
Modified
Mathlib/Order/ModularLattice.lean
modified
theorem
Disjoint.isCompl_sup_left_of_isCompl_sup_right
modified
theorem
Disjoint.isCompl_sup_right_of_isCompl_sup_left