Commit 2024-11-25 11:04 a3580b7e

View on Github →

chore(Order/ConditionallyCompleteLattice): split off Defs.lean from Basic.lean (#19277)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

deleted def conditionallyCompleteLatticeOfLatticeOfsInf

deleted def conditionallyCompleteLatticeOfLatticeOfsSup

deleted def conditionallyCompleteLatticeOfsInf

deleted def conditionallyCompleteLatticeOfsSup

Created Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

added def conditionallyCompleteLatticeOfLatticeOfsInf

added def conditionallyCompleteLatticeOfLatticeOfsSup

added def conditionallyCompleteLatticeOfsInf

added def conditionallyCompleteLatticeOfsSup

Modified scripts/noshake.json