mathlib3
facc1d2d - feat(topology/algebra): topology on a linear_ordered_comm_group_with_zero (#9537)

Commit

4 years ago

feat(topology/algebra): topology on a linear_ordered_comm_group_with_zero (#9537) This is a modernized version of code from the perfectoid spaces project.

Author

PatrickMassot

Parents

b534feda

mathlib3 facc1d2d - feat(topology/algebra): topology on a linear_ordered_comm_group_with_zero (#9537)

mathlib3
facc1d2d - feat(topology/algebra): topology on a linear_ordered_comm_group_with_zero (#9537)