chore(ring_theory/unique_factorization_domain): drop simp annotation …

…for factors_pow (#14646) Followup to #14555.
leanprover-community · Jun 9, 2022 · 4d4de43 · 4d4de43
1 parent 7b4680f
commit 4d4de43
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/unique_factorization_domain.lean b/src/ring_theory/unique_factorization_domain.lean
@@ -461,7 +461,7 @@ begin
   exact (associated.mul_mul (factors_prod hx) (factors_prod hy)).symm,
 end
 
-@[simp] lemma factors_pow {x : α} (n : ℕ) :
+lemma factors_pow {x : α} (n : ℕ) :
   multiset.rel associated (factors (x ^ n)) (n • factors x) :=
 begin
   induction n with n ih,