deprecation

Author: kim-em

Mathlib/Algebra/GroupWithZero/Torsion.lean

@@ -27,7 +27,7 @@ theorem IsMulTorsionFree.mk' (ih : ∀ x ≠ 0, ∀ y ≠ 0, ∀ n ≠ 0, (x ^ n
   refine ⟨fun n hn x y hxy ↦ ?_⟩
   by_cases h : x ≠ 0 ∧ y ≠ 0
   · exact ih x h.1 y h.2 n hn hxy
-  grind [pow_eq_zero, zero_pow]
+  grind [eq_zero_of_pow_eq_zero, zero_pow]
 
 variable [UniqueFactorizationMonoid M] [NormalizationMonoid M] [IsMulTorsionFree Mˣ]