lattice_group): Move from `algebra.lattice_ordered_group` (#10763)

Commit

4 years ago

move(algebra/order/lattice_group): Move from `algebra.lattice_ordered_group` (#10763) Rename `algebra.lattice_ordered_group` in `algebra/order/lattice_group`.

Author

YaelDillies

Parents

f727e126

mathlib f070a69b - move(algebra/order/lattice_group): Move from `algebra.lattice_ordered_group` (#10763)

mathlib
f070a69b - move(algebra/order/lattice_group): Move from `algebra.lattice_ordered_group` (#10763)