R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ Multiset.sum (Multiset.map (natDegree ∘ fun a => X - ↑C a) s) = ↑Multiset.card s

case h
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ ∀ (f : R[X]), f ∈ Multiset.map (fun a => X - ↑C a) s → Monic f
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ natDegree (prod (Multiset.map (fun a => X - ↑C a) s)) = ↑Multiset.card s
rw [natDegree_multiset_prod_of_monic, Multiset.map_map]
no goals
case h
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ ∀ (f : R[X]), f ∈ Multiset.map (fun a => X - ↑C a) s → Monic f
exact Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a