[Merged by Bors] - chore(algebra/big_operators): generalize map_prod to monoid_hom_class

src/algebra/big_operators/basic.lean

@@ -106,50 +106,70 @@ by simp only [sum_eq_multiset_sum, multiset.sum_map_singleton]
 
 end finset
 
-
 @[to_additive]
-lemma monoid_hom.map_prod [comm_monoid β] [comm_monoid γ] (g : β →* γ) (f : α → β) (s : finset α) :
+lemma map_prod [comm_monoid β] [comm_monoid γ] {G : Type*} [monoid_hom_class G β γ] (g : G)
+  (f : α → β) (s : finset α) :
   g (∏ x in s, f x) = ∏ x in s, g (f x) :=
-by simp only [finset.prod_eq_multiset_prod, g.map_multiset_prod, multiset.map_map]
+by simp only [finset.prod_eq_multiset_prod, map_multiset_prod, multiset.map_map]
 
-@[to_additive]
-lemma mul_equiv.map_prod [comm_monoid β] [comm_monoid γ] (g : β ≃* γ) (f : α → β) (s : finset α) :
-  g (∏ x in s, f x) = ∏ x in s, g (f x) :=
-g.to_monoid_hom.map_prod f s
+section deprecated
+
+/-- Deprecated: use `_root_.map_prod` instead. -/
+@[to_additive "Deprecated: use `_root_.map_sum` instead."]
+protected lemma monoid_hom.map_prod [comm_monoid β] [comm_monoid γ] (g : β →* γ) (f : α → β)
+  (s : finset α) : g (∏ x in s, f x) = ∏ x in s, g (f x) :=
+map_prod g f s
 
-lemma ring_hom.map_list_prod [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :
+/-- Deprecated: use `_root_.map_prod` instead. -/
+@[to_additive "Deprecated: use `_root_.map_sum` instead."]
+protected lemma mul_equiv.map_prod [comm_monoid β] [comm_monoid γ] (g : β ≃* γ) (f : α → β)
+  (s : finset α) : g (∏ x in s, f x) = ∏ x in s, g (f x) :=
+map_prod g f s
+
+/-- Deprecated: use `_root_.map_list_prod` instead. -/
+protected lemma ring_hom.map_list_prod [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :
   f l.prod = (l.map f).prod :=
-f.to_monoid_hom.map_list_prod l
+map_list_prod f l
 
-lemma ring_hom.map_list_sum [non_assoc_semiring β] [non_assoc_semiring γ]
+/-- Deprecated: use `_root_.map_list_sum` instead. -/
+protected lemma ring_hom.map_list_sum [non_assoc_semiring β] [non_assoc_semiring γ]
   (f : β →+* γ) (l : list β) :
   f l.sum = (l.map f).sum :=
-f.to_add_monoid_hom.map_list_sum l
+map_list_sum f l
+
+/-- A morphism into the opposite ring acts on the product by acting on the reversed elements.
 
-/-- A morphism into the opposite ring acts on the product by acting on the reversed elements -/
-lemma ring_hom.unop_map_list_prod [semiring β] [semiring γ] (f : β →+* γᵐᵒᵖ) (l : list β) :
-  mul_opposite.unop (f l.prod) = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
-f.to_monoid_hom.unop_map_list_prod l
+Deprecated: use `_root_.unop_map_list_prod` instead.
+-/
+protected lemma ring_hom.unop_map_list_prod [semiring β] [semiring γ] (f : β →+* γᵐᵒᵖ)
+  (l : list β) : mul_opposite.unop (f l.prod) = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
+unop_map_list_prod f l
 
-lemma ring_hom.map_multiset_prod [comm_semiring β] [comm_semiring γ] (f : β →+* γ)
+/-- Deprecated: use `_root_.map_multiset_prod` instead. -/
+protected lemma ring_hom.map_multiset_prod [comm_semiring β] [comm_semiring γ] (f : β →+* γ)
   (s : multiset β) :
   f s.prod = (s.map f).prod :=
-f.to_monoid_hom.map_multiset_prod s
+map_multiset_prod f s
 
-lemma ring_hom.map_multiset_sum [non_assoc_semiring β] [non_assoc_semiring γ]
+/-- Deprecated: use `_root_.map_multiset_sum` instead. -/
+protected lemma ring_hom.map_multiset_sum [non_assoc_semiring β] [non_assoc_semiring γ]
   (f : β →+* γ) (s : multiset β) :
   f s.sum = (s.map f).sum :=
-f.to_add_monoid_hom.map_multiset_sum s
+map_multiset_sum f s
 
-lemma ring_hom.map_prod [comm_semiring β] [comm_semiring γ] (g : β →+* γ) (f : α → β)
+/-- Deprecated: use `_root_.map_prod` instead. -/
+protected lemma ring_hom.map_prod [comm_semiring β] [comm_semiring γ] (g : β →+* γ) (f : α → β)
   (s : finset α) :
   g (∏ x in s, f x) = ∏ x in s, g (f x) :=
-g.to_monoid_hom.map_prod f s
+map_prod g f s
 
-lemma ring_hom.map_sum [non_assoc_semiring β] [non_assoc_semiring γ]
+/-- Deprecated: use `_root_.map_sum` instead. -/
+protected lemma ring_hom.map_sum [non_assoc_semiring β] [non_assoc_semiring γ]
   (g : β →+* γ) (f : α → β) (s : finset α) :
   g (∑ x in s, f x) = ∑ x in s, g (f x) :=
-g.to_add_monoid_hom.map_sum f s
+map_sum g f s
+
+end deprecated
 
 @[to_additive]
 lemma monoid_hom.coe_finset_prod [mul_one_class β] [comm_monoid γ] (f : α → β →* γ) (s : finset α) :

src/algebra/big_operators/multiset.lean

@@ -75,12 +75,13 @@ lemma pow_count [decidable_eq α] (a : α) : a ^ s.count a = (s.filter (eq a)).p
 by rw [filter_eq, prod_repeat]
 
 @[to_additive]
-lemma prod_hom [comm_monoid β] (s : multiset α) (f : α →* β) : (s.map f).prod = f s.prod :=
+lemma prod_hom [comm_monoid β] (s : multiset α) {F : Type*} [monoid_hom_class F α β] (f : F) :
+  (s.map f).prod = f s.prod :=
 quotient.induction_on s $ λ l, by simp only [l.prod_hom f, quot_mk_to_coe, coe_map, coe_prod]
 
 @[to_additive]
-lemma prod_hom' [comm_monoid β] (s : multiset ι) (f : α →* β) (g : ι → α) :
-  (s.map $ λ i, f $ g i).prod = f (s.map g).prod :=
+lemma prod_hom' [comm_monoid β] (s : multiset ι) {F : Type*} [monoid_hom_class F α β] (f : F)
+  (g : ι → α) : (s.map $ λ i, f $ g i).prod = f (s.map g).prod :=
 by { convert (s.map g).prod_hom f, exact (map_map _ _ _).symm }
 
 @[to_additive]
@@ -106,7 +107,7 @@ m.prod_hom₂ (*) mul_mul_mul_comm (mul_one _) _ _
 
 @[to_additive sum_map_nsmul]
 lemma prod_map_pow {n : ℕ} : (m.map $ λ i, f i ^ n).prod = (m.map f).prod ^ n :=
-m.prod_hom' (pow_monoid_hom n) _
+m.prod_hom' (@pow_monoid_hom α _ n) f
 
 @[to_additive]
 lemma prod_map_prod_map (m : multiset β) (n : multiset γ) {f : β → γ → α} :
@@ -198,21 +199,21 @@ variables [comm_group α] {m : multiset ι} {f g : ι → α}
 
 @[simp, to_additive]
 lemma prod_map_inv' : (m.map $ λ i, (f i)⁻¹).prod = (m.map f).prod ⁻¹ :=
-by { convert (m.map f).prod_hom comm_group.inv_monoid_hom, rw map_map, refl }
+by { convert (m.map f).prod_hom (@comm_group.inv_monoid_hom α _), rw map_map, refl }
 
 @[simp, to_additive]
 lemma prod_map_div : (m.map $ λ i, f i / g i).prod = (m.map f).prod / (m.map g).prod :=
 m.prod_hom₂ (/) mul_div_comm' (div_one' _) _ _
 
 @[to_additive]
 lemma prod_map_zpow {n : ℤ} : (m.map $ λ i, f i ^ n).prod = (m.map f).prod ^ n :=
-by { convert (m.map f).prod_hom (zpow_group_hom _), rw map_map, refl }
+by { convert (m.map f).prod_hom (@zpow_group_hom α _ _), rw map_map, refl }
 
 @[simp] lemma coe_inv_monoid_hom : (comm_group.inv_monoid_hom : α → α) = has_inv.inv := rfl
 
 @[simp, to_additive]
 lemma prod_map_inv (m : multiset α) : (m.map has_inv.inv).prod = m.prod⁻¹ :=
-m.prod_hom comm_group.inv_monoid_hom
+m.prod_hom (@comm_group.inv_monoid_hom α _)
 
 end comm_group
 
@@ -221,14 +222,14 @@ variables [comm_group_with_zero α] {m : multiset ι} {f g : ι → α}
 
 @[simp]
 lemma prod_map_inv₀ : (m.map $ λ i, (f i)⁻¹).prod = (m.map f).prod ⁻¹ :=
-by { convert (m.map f).prod_hom inv_monoid_with_zero_hom.to_monoid_hom, rw map_map, refl }
+by { convert (m.map f).prod_hom (@inv_monoid_with_zero_hom α _), rw map_map, refl }
 
 @[simp]
 lemma prod_map_div₀ : (m.map $ λ i, f i / g i).prod = (m.map f).prod / (m.map g).prod :=
 m.prod_hom₂ (/) (λ _ _ _ _, (div_mul_div _ _ _ _).symm) (div_one _) _ _
 
 lemma prod_map_zpow₀ {n : ℤ} : prod (m.map $ λ i, f i ^ n) = (m.map f).prod ^ n :=
-by { convert (m.map f).prod_hom (zpow_group_hom₀ _), rw map_map, refl }
+by { convert (m.map f).prod_hom (@zpow_group_hom₀ α _ _), rw map_map, refl }
 
 end comm_group_with_zero
 
@@ -398,6 +399,11 @@ le_sum_of_subadditive _ abs_zero abs_add s
 end multiset
 
 @[to_additive]
-lemma monoid_hom.map_multiset_prod [comm_monoid α] [comm_monoid β] (f : α →* β) (s : multiset α) :
-  f s.prod = (s.map f).prod :=
+lemma map_multiset_prod [comm_monoid α] [comm_monoid β] {F : Type*} [monoid_hom_class F α β]
+  (f : F) (s : multiset α) : f s.prod = (s.map f).prod :=
+(s.prod_hom f).symm
+
+@[to_additive]
+protected lemma monoid_hom.map_multiset_prod [comm_monoid α] [comm_monoid β] (f : α →* β)
+  (s : multiset α) : f s.prod = (s.map f).prod :=
 (s.prod_hom f).symm

src/algebra/polynomial/big_operators.lean

@@ -241,16 +241,16 @@ variables [comm_ring R]
 open monic
 -- Eventually this can be generalized with Vieta's formulas
 -- plus the connection between roots and factorization.
-lemma multiset_prod_X_sub_C_next_coeff [nontrivial R] (t : multiset R) :
+lemma multiset_prod_X_sub_C_next_coeff (t : multiset R) :
   next_coeff (t.map (λ x, X - C x)).prod = -t.sum :=
 begin
   rw next_coeff_multiset_prod,
   { simp only [next_coeff_X_sub_C],
-    refine t.sum_hom ⟨has_neg.neg, _, _⟩; simp [add_comm] },
+    exact t.sum_hom (-add_monoid_hom.id R) },
   { intros, apply monic_X_sub_C }
 end
 
-lemma prod_X_sub_C_next_coeff [nontrivial R] {s : finset ι} (f : ι → R) :
+lemma prod_X_sub_C_next_coeff {s : finset ι} (f : ι → R) :
   next_coeff ∏ i in s, (X - C (f i)) = -∑ i in s, f i :=
 by simpa using multiset_prod_X_sub_C_next_coeff (s.1.map f)
 

src/data/finsupp/basic.lean

@@ -1047,22 +1047,32 @@ end add_monoid
 end finsupp
 
 @[to_additive]
-lemma mul_equiv.map_finsupp_prod [has_zero M] [comm_monoid N] [comm_monoid P]
+lemma map_finsupp_prod [has_zero M] [comm_monoid N] [comm_monoid P] {H : Type*}
+  [monoid_hom_class H N P] (h : H) (f : α →₀ M) (g : α → M → N) :
+  h (f.prod g) = f.prod (λ a b, h (g a b)) :=
+map_prod h _ _
+
+/-- Deprecated, use `_root_.map_finsupp_prod` instead. -/
+@[to_additive "Deprecated, use `_root_.map_finsupp_sum` instead."]
+protected lemma mul_equiv.map_finsupp_prod [has_zero M] [comm_monoid N] [comm_monoid P]
   (h : N ≃* P) (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod (λ a b, h (g a b)) :=
-h.map_prod _ _
+map_finsupp_prod h f g
 
-@[to_additive]
-lemma monoid_hom.map_finsupp_prod [has_zero M] [comm_monoid N] [comm_monoid P]
+/-- Deprecated, use `_root_.map_finsupp_prod` instead. -/
+@[to_additive "Deprecated, use `_root_.map_finsupp_sum` instead."]
+protected lemma monoid_hom.map_finsupp_prod [has_zero M] [comm_monoid N] [comm_monoid P]
   (h : N →* P) (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod (λ a b, h (g a b)) :=
-h.map_prod _ _
+map_finsupp_prod h f g
 
-lemma ring_hom.map_finsupp_sum [has_zero M] [semiring R] [semiring S]
+/-- Deprecated, use `_root_.map_finsupp_sum` instead. -/
+protected lemma ring_hom.map_finsupp_sum [has_zero M] [semiring R] [semiring S]
   (h : R →+* S) (f : α →₀ M) (g : α → M → R) : h (f.sum g) = f.sum (λ a b, h (g a b)) :=
-h.map_sum _ _
+map_finsupp_sum h f g
 
-lemma ring_hom.map_finsupp_prod [has_zero M] [comm_semiring R] [comm_semiring S]
+/-- Deprecated, use `_root_.map_finsupp_prod` instead. -/
+protected lemma ring_hom.map_finsupp_prod [has_zero M] [comm_semiring R] [comm_semiring S]
   (h : R →+* S) (f : α →₀ M) (g : α → M → R) : h (f.prod g) = f.prod (λ a b, h (g a b)) :=
-h.map_prod _ _
+map_finsupp_prod h f g
 
 @[to_additive]
 lemma monoid_hom.coe_finsupp_prod [has_zero β] [monoid N] [comm_monoid P]
@@ -1204,7 +1214,7 @@ finset.prod_mul_distrib
 @[simp, to_additive]
 lemma prod_inv [has_zero M] [comm_group G] {f : α →₀ M}
   {h : α → M → G} : f.prod (λa b, (h a b)⁻¹) = (f.prod h)⁻¹ :=
-(((monoid_hom.id G)⁻¹).map_prod _ _).symm
+(map_prod ((monoid_hom.id G)⁻¹) _ _).symm
 
 @[simp] lemma sum_sub [has_zero M] [add_comm_group G] {f : α →₀ M}
   {h₁ h₂ : α → M → G} :

src/data/list/big_operators.lean

@@ -52,10 +52,10 @@ lemma prod_hom_rel (l : list ι) {r : M → N → Prop} {f : ι → M} {g : ι 
 list.rec_on l h₁ (λ a l hl, by simp only [map_cons, prod_cons, h₂ hl])
 
 @[to_additive]
-lemma prod_hom (l : list M) (f : M →* N) :
+lemma prod_hom (l : list M) {F : Type*} [monoid_hom_class F M N] (f : F) :
   (l.map f).prod = f l.prod :=
-by { simp only [prod, foldl_map, f.map_one.symm],
-  exact l.foldl_hom _ _ _ 1 f.map_mul }
+by { simp only [prod, foldl_map, ← map_one f],
+  exact l.foldl_hom _ _ _ 1 (map_mul f) }
 
 @[to_additive]
 lemma prod_hom₂ (l : list ι) (f : M → N → P)
@@ -74,7 +74,7 @@ lemma prod_map_mul {α : Type*} [comm_monoid α] {l : list ι} {f g : ι → α}
 l.prod_hom₂ (*) mul_mul_mul_comm (mul_one _) _ _
 
 @[to_additive]
-lemma prod_map_hom (L : list ι) (f : ι → M) (g : M →* N) :
+lemma prod_map_hom (L : list ι) (f : ι → M) {G : Type*} [monoid_hom_class G M N] (g : G) :
   (L.map (g ∘ f)).prod = g ((L.map f).prod) :=
 by rw [← prod_hom, map_map]
 
@@ -443,18 +443,35 @@ by rw [← op_inj, op_unop, mul_opposite.op_list_prod, map_reverse, map_map, rev
 
 end mul_opposite
 
-namespace monoid_hom
+section monoid_hom
 
 variables [monoid M] [monoid N]
 
 @[to_additive]
-lemma map_list_prod (f : M →* N) (l : list M) :
-  f l.prod = (l.map f).prod :=
+lemma map_list_prod {F : Type*} [monoid_hom_class F M N] (f : F)
+  (l : list M) : f l.prod = (l.map f).prod :=
 (l.prod_hom f).symm
 
-/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements -/
-lemma unop_map_list_prod (f : M →* Nᵐᵒᵖ) (l : list M) :
+/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
+lemma unop_map_list_prod {F : Type*} [monoid_hom_class F M Nᵐᵒᵖ] (f : F) (l : list M) :
   (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
-by rw [f.map_list_prod l, mul_opposite.unop_list_prod, list.map_map]
+by rw [map_list_prod f l, mul_opposite.unop_list_prod, list.map_map]
+
+namespace monoid_hom
+
+/-- Deprecated, use `_root_.map_list_prod` instead. -/
+@[to_additive "Deprecated, use `_root_.map_list_sum` instead."]
+protected lemma map_list_prod (f : M →* N) (l : list M) :
+  f l.prod = (l.map f).prod :=
+map_list_prod f l
+
+/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements.
+
+Deprecated, use `_root_.unop_map_list_prod` instead. -/
+protected lemma unop_map_list_prod (f : M →* Nᵐᵒᵖ) (l : list M) :
+  (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
+unop_map_list_prod f l
+
+end monoid_hom
 
 end monoid_hom

src/data/polynomial/eval.lean

@@ -642,7 +642,7 @@ end
 lemma eval_map (x : S) : (p.map f).eval x = p.eval₂ f x :=
 eval₂_map f (ring_hom.id _) x
 
-lemma map_sum {ι : Type*} (g : ι → R[X]) (s : finset ι) :
+protected lemma map_sum {ι : Type*} (g : ι → R[X]) (s : finset ι) :
   (∑ i in s, g i).map f = ∑ i in s, (g i).map f :=
 (map_ring_hom f).map_sum _ _
 
@@ -794,10 +794,10 @@ section map
 
 variables [comm_semiring R] [comm_semiring S] (f : R →+* S)
 
-lemma map_multiset_prod (m : multiset R[X]) : m.prod.map f = (m.map $ map f).prod :=
+protected lemma map_multiset_prod (m : multiset R[X]) : m.prod.map f = (m.map $ map f).prod :=
 eq.symm $ multiset.prod_hom _ (map_ring_hom f).to_monoid_hom
 
-lemma map_prod {ι : Type*} (g : ι → R[X]) (s : finset ι) :
+protected lemma map_prod {ι : Type*} (g : ι → R[X]) (s : finset ι) :
   (∏ i in s, g i).map f = ∏ i in s, (g i).map f :=
 (map_ring_hom f).map_prod _ _
 

src/field_theory/splitting_field.lean

@@ -243,7 +243,7 @@ have h2 : (0 : L[X]) ∉ m.map (λ r, X - C (i r)),
 begin
   rw map_id at hm, rw hm at hf0 hmf0 ⊢, rw map_mul at hmf0 ⊢,
   rw [roots_mul hf0, roots_mul hmf0, map_C, roots_C, zero_add, roots_C, zero_add,
-      map_multiset_prod, multiset.map_map], simp_rw [(∘), map_sub, map_X, map_C],
+      polynomial.map_multiset_prod, multiset.map_map], simp_rw [(∘), map_sub, map_X, map_C],
   rw [roots_multiset_prod _ h2, multiset.bind_map,
       roots_multiset_prod _ h1, multiset.bind_map],
   simp_rw roots_X_sub_C,
@@ -407,7 +407,7 @@ lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq {K : Type*} [comm_ring K]
   (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
 begin
   apply map_injective _ (is_fraction_ring.injective K (fraction_ring K)),
-  rw map_multiset_prod,
+  rw polynomial.map_multiset_prod,
   simp only [map_C, function.comp_app, map_X, multiset.map_map, map_sub],
   have : p.roots.map (algebra_map K (fraction_ring K)) =
     (map (algebra_map K (fraction_ring K)) p).roots :=
@@ -458,7 +458,7 @@ begin
   have hcoeff : p.leading_coeff ≠ 0,
   { intro h, exact hzero (leading_coeff_eq_zero.1 h) },
   apply map_injective _ (is_fraction_ring.injective K (fraction_ring K)),
-  rw [map_mul, map_multiset_prod],
+  rw [map_mul, polynomial.map_multiset_prod],
   simp only [map_C, function.comp_app, map_X, multiset.map_map, map_sub],
   have h : p.roots.map (algebra_map K (fraction_ring K)) =
     (map (algebra_map K (fraction_ring K)) p).roots :=

src/order/filter/basic.lean

@@ -2639,7 +2639,7 @@ begin
   exact filter.prod_mono hf hg,
 end
 
-lemma map_prod (m : α × β → γ) (f : filter α) (g : filter β) :
+protected lemma map_prod (m : α × β → γ) (f : filter α) (g : filter β) :
   map m (f ×ᶠ g) = (f.map (λ a b, m (a, b))).seq g :=
 begin
   simp [filter.ext_iff, mem_prod_iff, mem_map_seq_iff],
@@ -2650,7 +2650,7 @@ begin
 end
 
 lemma prod_eq {f : filter α} {g : filter β} : f ×ᶠ g = (f.map prod.mk).seq g  :=
-have h : _ := map_prod id f g, by rwa [map_id] at h
+have h : _ := f.map_prod id g, by rwa [map_id] at h
 
 lemma prod_inf_prod {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
   (f₁ ×ᶠ g₁) ⊓ (f₂ ×ᶠ g₂) = (f₁ ⊓ f₂) ×ᶠ (g₁ ⊓ g₂) :=

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -390,7 +390,7 @@ lemma prod_cyclotomic_eq_X_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type*) [com
 begin
   have integer : ∏ i in nat.divisors n, cyclotomic i ℤ = X ^ n - 1,
   { apply map_injective (int.cast_ring_hom ℂ) int.cast_injective,
-    rw map_prod (int.cast_ring_hom ℂ) (λ i, cyclotomic i ℤ),
+    rw polynomial.map_prod (int.cast_ring_hom ℂ) (λ i, cyclotomic i ℤ),
     simp only [int_cyclotomic_spec, polynomial.map_pow, nat.cast_id, map_X, map_one, map_sub],
     exact prod_cyclotomic'_eq_X_pow_sub_one hpos
           (complex.is_primitive_root_exp n (ne_of_lt hpos).symm) },
@@ -399,8 +399,8 @@ begin
   have h : ∀ i ∈ n.divisors, cyclotomic i R = map (int.cast_ring_hom R) (cyclotomic i ℤ),
   { intros i hi,
     exact (map_cyclotomic_int i R).symm },
-  rw [finset.prod_congr (refl n.divisors) h, coerc, ←map_prod (int.cast_ring_hom R)
-                                                    (λ i, cyclotomic i ℤ), integer]
+  rw [finset.prod_congr (refl n.divisors) h, coerc,
+      ← polynomial.map_prod (int.cast_ring_hom R) (λ i, cyclotomic i ℤ), integer]
 end
 
 lemma cyclotomic.dvd_X_pow_sub_one (n : ℕ) (R : Type*) [comm_ring R] :