Commit 2021-12-03 16:11 1e18e93d

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).