feat: port Algebra.Order.Hom.Ring (#1482)

Worked around #2505, but finally everything works.
leanprover-community · Feb 27, 2023 · 19b42dd · 19b42dd
1 parent 13f9beb
commit 19b42dd
Show file tree

Hide file tree

Showing 2 changed files with 601 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -141,6 +141,7 @@ import Mathlib.Algebra.Order.Group.Units
 import Mathlib.Algebra.Order.Group.WithTop
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Hom.Monoid
+import Mathlib.Algebra.Order.Hom.Ring
 import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.LatticeGroup