chore(data/polynomial/field_division): beta-reduce (#10835)

leanprover-community · Dec 16, 2021 · 8e4b3b0 · 8e4b3b0
1 parent 5a835b7
commit 8e4b3b0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
@@ -429,7 +429,7 @@ end
 
 lemma prod_multiset_root_eq_finset_root (p : polynomial R) :
   (multiset.map (λ (a : R), X - C a) p.roots).prod =
-  ∏ a in (multiset.to_finset p.roots), (λ (a : R), (X - C a) ^ (root_multiplicity a p)) a :=
+  ∏ a in p.roots.to_finset, (X - C a) ^ root_multiplicity a p :=
 by simp only [count_roots, finset.prod_multiset_map_count]
 
 /-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/