R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - ↑C (↑f a)) ^ rootMultiplicity a p ∣ map f p
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ rootMultiplicity a p ≤ rootMultiplicity (↑f a) (map f p)
rw [le_rootMultiplicity_iff hmap]
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - ↑C (↑f a)) ^ rootMultiplicity a p ∣ ↑(mapRingHom f) ((X - ↑C a) ^ rootMultiplicity a p)
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - ↑C (↑f a)) ^ rootMultiplicity a p ∣ map f p
refine' _root_.trans _ ((mapRingHom f).map_dvd (pow_rootMultiplicity_dvd p a))
no goals
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - ↑C (↑f a)) ^ rootMultiplicity a p ∣ ↑(mapRingHom f) ((X - ↑C a) ^ rootMultiplicity a p)
rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]