case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p k : R[X]
h : p * k ≠ 0
⊢ roots p ≤ roots (p * k)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : q ≠ 0
⊢ p ∣ q → roots p ≤ roots q
rintro ⟨k, rfl⟩
no goals
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p k : R[X]
h : p * k ≠ 0
⊢ roots p ≤ roots (p * k)
exact Multiset.le_iff_exists_add.mpr ⟨k.roots, roots_mul h⟩