feat: port Algebra.Order.Rearrangement (#2268)

Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
leanprover-community · Apr 10, 2023 · 9e9dfc2 · 9e9dfc2
1 parent 28c8a70
commit 9e9dfc2
Show file tree

Hide file tree

Showing 2 changed files with 547 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -211,6 +211,7 @@ import Mathlib.Algebra.Order.Pi
 import Mathlib.Algebra.Order.Pointwise
 import Mathlib.Algebra.Order.Positive.Field
 import Mathlib.Algebra.Order.Positive.Ring
+import Mathlib.Algebra.Order.Rearrangement
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Algebra.Order.Ring.Canonical
 import Mathlib.Algebra.Order.Ring.CharZero