feat(algebra/lattice_ordered_group): add basic theory of lattice ordered groups (#8673)

Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Author: mans0954

docs/references.bib

@@ -80,6 +80,13 @@ @Book{            axler2015
   publisher     = {Springer}
 }
 
+@Manual{          banasiak,
+  author        = {Banasiak},
+  title         = {Banach Lattices in Applications},
+  organization  = {University of Pretoria},
+  address       = {Pretoria, South Africa}
+}
+
 @Book{            beals2004,
   author        = {Richard Beals},
   title         = {Analysis. An introduction},
@@ -137,6 +144,22 @@ @Book{            billingsley1999
   url           = {https://doi.org/10.1002/9780470316962}
 }
 
+@Article{         birkhoff1942,
+  author        = {Birkhoff, Garrett},
+  title         = {Lattice, ordered groups},
+  journal       = {Ann. of Math. (2)},
+  fjournal      = {Annals of Mathematics. Second Series},
+  volume        = {43},
+  year          = {1942},
+  pages         = {298--331},
+  issn          = {0003-486X},
+  mrclass       = {20.0X},
+  mrnumber      = {6550},
+  mrreviewer    = {H. Wallman},
+  doi           = {10.2307/1968871},
+  url           = {https://doi.org/10.2307/1968871}
+}
+
 @Book{            borceux-vol1,
   title         = {Handbook of Categorical Algebra: Volume 1, Basic Category
                   Theory},
@@ -210,6 +233,19 @@ @Book{            bourbaki1975b
   mrnumber      = {2109105}
 }
 
+@Book{            bourbaki1981,
+  author        = {Bourbaki, N.},
+  title         = {Algebra. {II}. {C}hapters 4--7},
+  series        = {Elements of Mathematics (Berlin)},
+  note          = {Translated from the French by P. M. Cohn and J. Howie},
+  publisher     = {Springer-Verlag, Berlin},
+  year          = {1990},
+  pages         = {vii+461},
+  isbn          = {3-540-19375-8},
+  mrclass       = {00A05 (12-01 13-01)},
+  mrnumber      = {1080964}
+}
+
 @Article{         cadiou1972,
   title         = {Recursive definitions of partial functions and their
                   computations},
@@ -432,6 +468,19 @@ @InProceedings{   flypitch_itp
                   continuum hypothesis, Boolean-valued models, Lean}
 }
 
+@Book{            fuchs1963,
+  author        = {Fuchs, L.},
+  title         = {Partially ordered algebraic systems},
+  publisher     = {Pergamon Press, Oxford-London-New York-Paris;
+                  Addison-Wesley Publishing Co., Inc., Reading, Mass.-Palo
+                  Alto, Calif.-London},
+  year          = {1963},
+  pages         = {ix+229},
+  mrclass       = {06.00 (20.00)},
+  mrnumber      = {0171864},
+  mrreviewer    = {P. F. Conrad}
+}
+
 @InProceedings{   fuerer-lochbihler-schneider-traytel2020,
   author        = {Basil F{\"{u}}rer and Andreas Lochbihler and Joshua
                   Schneider and Dmitriy Traytel},
@@ -1190,6 +1239,14 @@ @Misc{            wedhorn_adic
   eprint        = {arXiv:1910.05934}
 }
 
+@TechReport{      zaanen1966,
+  author        = {Zaanen, A. C.},
+  title         = {Lectures on "Riesz Spaces"},
+  institution   = {Euratom},
+  year          = {1966},
+  number        = {EUR 3140.e}
+}
+
 @Article{         zbMATH06785026,
   author        = {John F. {Clauser} and Michael A. {Horne} and Abner
                   {Shimony} and Richard A. {Holt}},

src/algebra/field_power.lean

@@ -159,7 +159,7 @@ lemma fpow_even_abs (a : K) {p : ℤ} (hp : even p) :
   abs a ^ p = a ^ p :=
 begin
   cases le_or_lt a (-a) with h h;
-  simp [abs, h, max_eq_left_of_lt, fpow_even_neg _ hp]
+  simp [abs_eq_max_neg, h, max_eq_left_of_lt, fpow_even_neg _ hp]
 end
 
 @[simp] lemma fpow_bit0_abs (a : K) (p : ℤ) :

src/algebra/group/basic.lean

@@ -451,6 +451,11 @@ by rw [mul_inv_rev, mul_comm]
 lemma div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c :=
 by rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
 
+@[to_additive]
+lemma div_mul_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
+by rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_assoc,
+  mul_left_cancel_iff, mul_comm, mul_assoc]
+
 end comm_group
 
 section add_comm_group