Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_add_int_smul_mem_Ico

Modification history

2021-11-16 08:37
src/algebra/order/archimedean.lean
feat(algebra/order/archimedean): upgrade some `∃` to `∃!` (#10343)
Deleted exists_add_int_smul_mem_IcoView on Github →
2021-10-27 17:47
src/algebra/order/archimedean.lean
feat(algebra/order/archimedean): a few more lemmas (#9997) …
Added exists_add_int_smul_mem_IcoView on Github →