chore(ring_theory/hahn_series, topology/locally_constant/algebra): ad…

…d missing `non_unital_non_assoc_ring` instances (#13504)
leanprover-community · Apr 18, 2022 · 37d02d3 · 37d02d3
1 parent 3c20253
commit 37d02d3
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 0 deletions.
diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean
@@ -753,6 +753,18 @@ instance [comm_semiring R] : comm_semiring (hahn_series Γ R) :=
   end,
   .. hahn_series.semiring }
 
+instance [non_unital_non_assoc_ring R] : non_unital_non_assoc_ring (hahn_series Γ R) :=
+{ .. hahn_series.non_unital_non_assoc_semiring,
+  .. hahn_series.add_group }
+
+instance [non_unital_ring R] : non_unital_ring (hahn_series Γ R) :=
+{ .. hahn_series.non_unital_non_assoc_ring,
+  .. hahn_series.non_unital_semiring }
+
+instance [non_assoc_ring R] : non_assoc_ring (hahn_series Γ R) :=
+{ .. hahn_series.non_unital_non_assoc_ring,
+  .. hahn_series.non_assoc_semiring }
+
 instance [ring R] : ring (hahn_series Γ R) :=
 { .. hahn_series.semiring,
   .. hahn_series.add_comm_group }

diff --git a/src/topology/locally_constant/algebra.lean b/src/topology/locally_constant/algebra.lean
@@ -136,6 +136,16 @@ instance [semiring Y] : semiring (locally_constant X Y) :=
 instance [comm_semiring Y] : comm_semiring (locally_constant X Y) :=
 { .. locally_constant.semiring, .. locally_constant.comm_monoid }
 
+instance [non_unital_non_assoc_ring Y] : non_unital_non_assoc_ring (locally_constant X Y) :=
+{ .. locally_constant.add_comm_group, .. locally_constant.has_mul,
+  .. locally_constant.distrib, .. locally_constant.mul_zero_class }
+
+instance [non_unital_ring Y] : non_unital_ring (locally_constant X Y) :=
+{ .. locally_constant.semigroup, .. locally_constant.non_unital_non_assoc_ring }
+
+instance [non_assoc_ring Y] : non_assoc_ring (locally_constant X Y) :=
+{ .. locally_constant.mul_one_class, .. locally_constant.non_unital_non_assoc_ring }
+
 instance [ring Y] : ring (locally_constant X Y) :=
 { .. locally_constant.semiring, .. locally_constant.add_comm_group }