R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ (X - ↑C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)
rw [le_rootMultiplicity_iff hzero]
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
hdivp : (X - ↑C a) ^ rootMultiplicity a p ∣ p
⊢ (X - ↑C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ (X - ↑C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
have hdivp : (X - C a) ^ rootMultiplicity a p ∣ p := pow_rootMultiplicity_dvd p a
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
hdivp : (X - ↑C a) ^ rootMultiplicity a p ∣ p
hdivq : (X - ↑C a) ^ rootMultiplicity a q ∣ q
⊢ (X - ↑C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
hdivp : (X - ↑C a) ^ rootMultiplicity a p ∣ p
⊢ (X - ↑C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
have hdivq : (X - C a) ^ rootMultiplicity a q ∣ q := pow_rootMultiplicity_dvd q a
no goals
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
hdivp : (X - ↑C a) ^ rootMultiplicity a p ∣ p
hdivq : (X - ↑C a) ^ rootMultiplicity a q ∣ q
⊢ (X - ↑C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
exact min_pow_dvd_add hdivp hdivq