linear_locally_finite): there is an order_iso between a linear locally finite order and a subset of Z (#16832)

Commit

3 years ago

feat(order/succ_pred/linear_locally_finite): there is an order_iso between a linear locally finite order and a subset of Z (#16832) Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author

RemyDegenne

Parents

ed98c07f

mathlib 2647cabe - feat(order/succ_pred/linear_locally_finite): there is an order_iso between a linear locally finite order and a subset of Z (#16832)

mathlib
2647cabe - feat(order/succ_pred/linear_locally_finite): there is an order_iso between a linear locally finite order and a subset of Z (#16832)