Commit 2021-10-27 17:47 8ce5da4b
View on Github →feat(algebra/order/archimedean): a few more lemmas (#9997)
Prove that a + m • b ∈ Ioc c (c + b) for some m : ℤ, and similarly for Ico.
Also move some lemmas out of a namespace.
feat(algebra/order/archimedean): a few more lemmas (#9997)
Prove that a + m • b ∈ Ioc c (c + b) for some m : ℤ, and similarly for Ico.
Also move some lemmas out of a namespace.