diff --git a/Mathlib/Algebra/Group/Pi/Basic.lean b/Mathlib/Algebra/Group/Pi/Basic.lean
index 88e48e69be7ae0..fbf10471b31bb8 100644
--- a/Mathlib/Algebra/Group/Pi/Basic.lean
+++ b/Mathlib/Algebra/Group/Pi/Basic.lean
@@ -64,6 +64,11 @@ instance mulOneClass [∀ i, MulOneClass (f i)] : MulOneClass (∀ i, f i) where
   one_mul := by intros; ext; exact one_mul _
   mul_one := by intros; ext; exact mul_one _
 
+@[to_additive]
+instance [∀ i, MulOneClass (f i)] [∀ i, IsDedekindFiniteMonoid (f i)] :
+    IsDedekindFiniteMonoid (∀ i, f i) where
+  mul_eq_one_symm := by simp [funext_iff, mul_eq_one_comm]
+
 @[to_additive]
 instance invOneClass [∀ i, InvOneClass (f i)] : InvOneClass (∀ i, f i) where
   inv_one := by ext; exact inv_one
diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean
index 12b8deaed8d2d4..7436fb680d17d8 100644
--- a/Mathlib/Algebra/Group/Prod.lean
+++ b/Mathlib/Algebra/Group/Prod.lean
@@ -85,6 +85,11 @@ instance instMulOneClass [MulOneClass M] [MulOneClass N] : MulOneClass (M × N)
   one_mul _ := by ext <;> exact one_mul _
   mul_one _ := by ext <;> exact mul_one _
 
+@[to_additive]
+instance [MulOneClass M] [MulOneClass N] [IsDedekindFiniteMonoid M] [IsDedekindFiniteMonoid N] :
+    IsDedekindFiniteMonoid (M × N) where
+  mul_eq_one_symm := by simp [mul_eq_one_comm]
+
 @[to_additive]
 instance instMonoid [Monoid M] [Monoid N] : Monoid (M × N) :=
   { npow := fun z a => ⟨NPow.npow z a.1, NPow.npow z a.2⟩,