chore(data/mv_polynomial): mark mv_polynomial.ext as @[ext] (#5289)

leanprover-community · Dec 9, 2020 · d12a731 · d12a731
1 parent 1f309c5
commit d12a731
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean
@@ -297,7 +297,7 @@ local attribute [reducible] mv_polynomial
 def coeff (m : σ →₀ ℕ) (p : mv_polynomial σ R) : R := p m
 end
 
-lemma ext (p q : mv_polynomial σ R) :
+@[ext] lemma ext (p q : mv_polynomial σ R) :
   (∀ m, coeff m p = coeff m q) → p = q := ext
 
 lemma ext_iff (p q : mv_polynomial σ R) :