R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ map (algebraMap R (FractionRing R)) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))) ∣
    map (algebraMap R (FractionRing R)) p
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)) ∣ p
rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R) monic_prod_multiset_X_sub_C]
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ (Finset.prod (Multiset.toFinset (roots p)) fun i =>
      map (algebraMap R (FractionRing R)) ((X - ↑C i) ^ rootMultiplicity i p)) ∣
    map (algebraMap R (FractionRing R)) p
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ map (algebraMap R (FractionRing R)) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))) ∣
    map (algebraMap R (FractionRing R)) p
rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
case refine'_1
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
a : R
x✝¹ : a ∈ ↑(Multiset.toFinset (roots p))
b : R
x✝ : b ∈ ↑(Multiset.toFinset (roots p))
h : a ≠ b
⊢ (IsCoprime on fun i => map (algebraMap R (FractionRing R)) ((X - ↑C i) ^ rootMultiplicity i p)) a b

case refine'_2
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
a : R
x✝ : a ∈ Multiset.toFinset (roots p)
⊢ map (algebraMap R (FractionRing R)) ((X - ↑C a) ^ rootMultiplicity a p) ∣ map (algebraMap R (FractionRing R)) p
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ (Finset.prod (Multiset.toFinset (roots p)) fun i =>
      map (algebraMap R (FractionRing R)) ((X - ↑C i) ^ rootMultiplicity i p)) ∣
    map (algebraMap R (FractionRing R)) p
refine' Finset.prod_dvd_of_coprime (fun a _ b _ h => _) fun a _ => _
case refine'_1
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
a : R
x✝¹ : a ∈ ↑(Multiset.toFinset (roots p))
b : R
x✝ : b ∈ ↑(Multiset.toFinset (roots p))
h : a ≠ b
⊢ (IsCoprime on fun i => (X - ↑C (↑(algebraMap R (FractionRing R)) i)) ^ rootMultiplicity i p) a b
case refine'_1
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
a : R
x✝¹ : a ∈ ↑(Multiset.toFinset (roots p))
b : R
x✝ : b ∈ ↑(Multiset.toFinset (roots p))
h : a ≠ b
⊢ (IsCoprime on fun i => map (algebraMap R (FractionRing R)) ((X - ↑C i) ^ rootMultiplicity i p)) a b
simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
no goals
case refine'_1
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
a : R
x✝¹ : a ∈ ↑(Multiset.toFinset (roots p))
b : R
x✝ : b ∈ ↑(Multiset.toFinset (roots p))
h : a ≠ b
⊢ (IsCoprime on fun i => (X - ↑C (↑(algebraMap R (FractionRing R)) i)) ^ rootMultiplicity i p) a b
exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
no goals
case refine'_2
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
a : R
x✝ : a ∈ Multiset.toFinset (roots p)
⊢ map (algebraMap R (FractionRing R)) ((X - ↑C a) ^ rootMultiplicity a p) ∣ map (algebraMap R (FractionRing R)) p
exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)