case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : P = 0
⊢ degree (Polynomial.map f P) = degree P

case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree (Polynomial.map f P) = degree P
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ degree (Polynomial.map f P) = degree P
by_cases hP : P = 0
no goals
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : P = 0
⊢ degree (Polynomial.map f P) = degree P
simp [hP]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree P ≤ degree (Polynomial.map f P)
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree (Polynomial.map f P) = degree P
refine' le_antisymm (degree_map_le _ _) _
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ ↑(natDegree P) ≤ degree (Polynomial.map f P)
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree P ≤ degree (Polynomial.map f P)
rw [degree_eq_natDegree hP]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ ↑(natDegree P) ≤ degree (Polynomial.map f P)
refine' le_degree_of_ne_zero _
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ 1 ≠ 0
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
no goals
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ 1 ≠ 0
exact one_ne_zero