mathlib3

75cfbb3c - chore(algebra/lattice_ordered_group): review (names, spaces, golf...) (#10595)

chore(algebra/lattice_ordered_group): review (names, spaces, golf...) (#10595) This is a review of `algebra/lattice_ordered_group` and `analysis/normed_space/lattice_ordered_group`: - delete or add spaces at many places - add brackets around goals - replace `apply` by `exact` when closing a goal - change many names to better fit the naming convention - cut some big proofs into several lemmas - add a few `simp` attributes - remove a non-terminal simp - golf - add some simple API lemmas I did not do anything about the docstrings of the lemmas. Some of them don't interact correctly with `to_additive` (the additive comment is shown for the multiplicative lemma in the doc, for example).