2021-12-03 20:46
src/algebra/lattice_ordered_group.lean
feat(analysis.normed_space.lattice_ordered_group): Add `two_inf_sub_two_inf_le`, `two_sup_sub_two_sup_le` and supporting lemmas (#10514) …
Deleted lattice_ordered_comm_group.two_inf_eq_mul_div_abs_div