From 37d02d3da4e6d8437d522174bf85276fcd882b54 Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Mon, 18 Apr 2022 20:47:04 +0000
Subject: [PATCH] chore(ring_theory/hahn_series,
 topology/locally_constant/algebra): add missing `non_unital_non_assoc_ring`
 instances (#13504)

---
 src/ring_theory/hahn_series.lean           | 12 ++++++++++++
 src/topology/locally_constant/algebra.lean | 10 ++++++++++
 2 files changed, 22 insertions(+)

diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean
index 3c66dc89d2beb..74db2ffa13ecc 100644
--- 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
index 36d369c02ffcf..577481f4ec6cf 100644
--- 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 }