Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-12 08:56
90cf978d
View on Github →
chore(Order/Bounds): move defs to a new file (
#17676
) Also generalize definitions to
LE
.
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/CharP/Defs.lean
Modified
Mathlib/Data/Int/GCD.lean
Modified
Mathlib/Order/Bounds/Basic.lean
deleted
def
BddAbove
deleted
def
BddBelow
deleted
def
IsGLB
deleted
def
IsGreatest
deleted
def
IsLUB
deleted
def
IsLeast
deleted
def
lowerBounds
deleted
def
upperBounds
Created
Mathlib/Order/Bounds/Defs.lean
added
def
BddAbove
added
def
BddBelow
added
def
IsGLB
added
def
IsGreatest
added
def
IsLUB
added
def
IsLeast
added
def
lowerBounds
added
def
upperBounds
Modified
Mathlib/Order/WellFounded.lean