mathlib3
5021c1f9 - feat(data/int): conditionally complete linear order (#8149)

Commit
4 years ago
feat(data/int): conditionally complete linear order (#8149) Prove that the integers form a conditionally complete linear order. I do not have a specific goal in mind for this, but it would have been helpful to formulate one of the Proof Ground problems using this. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading