case pos
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
hf : Function.Injective ↑f
a : A
hp0 : p = 0
⊢ rootMultiplicity a p = rootMultiplicity (↑f a) (map f p)

case neg
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
hf : Function.Injective ↑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity a p = rootMultiplicity (↑f a) (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
hf : Function.Injective ↑f
a : A
⊢ rootMultiplicity a p = rootMultiplicity (↑f a) (map f p)
by_cases hp0 : p = 0
case neg
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
hf : Function.Injective ↑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity (↑f a) (map f p) ≤ rootMultiplicity a p
case neg
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
hf : Function.Injective ↑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity a p = rootMultiplicity (↑f a) (map f p)
apply le_antisymm (le_rootMultiplicity_map ((Polynomial.map_ne_zero_iff hf).mpr hp0) a)
case neg
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
hf : Function.Injective ↑f
a : A
hp0 : ¬p = 0
⊢ (X - ↑C (↑f a)) ^ rootMultiplicity (↑f a) (map f p) ∣ map f p
case neg
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
hf : Function.Injective ↑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity (↑f a) (map f p) ≤ rootMultiplicity a p
rw [le_rootMultiplicity_iff hp0, ← map_dvd_map f hf ((monic_X_sub_C a).pow _),
  Polynomial.map_pow, Polynomial.map_sub, map_X, map_C]
no goals
case neg
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
hf : Function.Injective ↑f
a : A
hp0 : ¬p = 0
⊢ (X - ↑C (↑f a)) ^ rootMultiplicity (↑f a) (map f p) ∣ map f p
apply pow_rootMultiplicity_dvd
no goals
case pos
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
hf : Function.Injective ↑f
a : A
hp0 : p = 0
⊢ rootMultiplicity a p = rootMultiplicity (↑f a) (map f p)
simp only [hp0, rootMultiplicity_zero, Polynomial.map_zero]