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
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
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
⊢ natDegree (Polynomial.map f P) = natDegree P
refine' le_antisymm (natDegree_map_le _ _) (le_natDegree_of_ne_zero _)
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
⊢ 1 ≠ 0
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
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
no goals
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
⊢ 1 ≠ 0
exact one_ne_zero