R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ degree p ≤ degree (map f p)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
⊢ degree p ≤ degree (map f p)
have hp0 : p ≠ 0 :=
  leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ ↑(natDegree p) ≤ degree (map f p)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ degree p ≤ degree (map f p)
rw [degree_eq_natDegree hp0]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ coeff (map f p) (natDegree p) ≠ 0
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ ↑(natDegree p) ≤ degree (map f p)
refine' le_degree_of_ne_zero _
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ ↑f (coeff p (natDegree p)) ≠ 0
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ coeff (map f p) (natDegree p) ≠ 0
rw [coeff_map]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ ↑f (coeff p (natDegree p)) ≠ 0
exact hf