no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : p = 0
⊢ degree (map f p) = degree p
simp [h]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : ¬p = 0
⊢ ↑f (leadingCoeff p) ≠ ↑f 0
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : ¬p = 0
⊢ ↑f (leadingCoeff p) ≠ 0
rw [← f.map_zero]
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : ¬p = 0
⊢ ↑f (leadingCoeff p) ≠ ↑f 0
exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h)