feat: add missing NonAssocRing, Ring and CommRing instances for…

… `Unitization` (#5101)
leanprover-community · Jun 16, 2023 · 4acf4c1 · 4acf4c1
1 parent 0783216
commit 4acf4c1
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Algebra/Unitization.lean b/Mathlib/Algebra/Algebra/Unitization.lean
@@ -497,6 +497,18 @@ instance commSemiring [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] [I
     [SMulCommClass R A A] : CommSemiring (Unitization R A) :=
   { Unitization.commMonoid, Unitization.nonAssocSemiring with }
 
+instance nonAssocRing [CommRing R] [NonUnitalNonAssocRing A] [Module R A] :
+    NonAssocRing (Unitization R A) :=
+  { Unitization.addCommGroup, Unitization.nonAssocSemiring with }
+
+instance ring [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A]
+    [SMulCommClass R A A] : Ring (Unitization R A) :=
+  { Unitization.addCommGroup, Unitization.semiring with }
+
+instance commRing [CommRing R] [NonUnitalCommRing A] [Module R A] [IsScalarTower R A A]
+    [SMulCommClass R A A] : CommRing (Unitization R A) :=
+  { Unitization.addCommGroup, Unitization.commSemiring with }
+
 variable (R A)
 
 /-- The canonical inclusion of rings `R →+* Unitization R A`. -/