case mk
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
m : Multiset R[X]
L : List R[X]
⊢ ¬0 ∈ Quot.mk Setoid.r L → roots (prod (Quot.mk Setoid.r L)) = Multiset.bind (Quot.mk Setoid.r L) roots
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
m : Multiset R[X]
⊢ ¬0 ∈ m → roots (prod m) = Multiset.bind m roots
rcases m with ⟨L⟩
no goals
case mk
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
m : Multiset R[X]
L : List R[X]
⊢ ¬0 ∈ Quot.mk Setoid.r L → roots (prod (Quot.mk Setoid.r L)) = Multiset.bind (Quot.mk Setoid.r L) roots
simpa only [Multiset.coe_prod, quot_mk_to_coe''] using roots_list_prod L