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]
⊢ coeff (map f p) (natDegree (map f p)) = ↑f (coeff p (natDegree p))
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]
⊢ leadingCoeff (map f p) = ↑f (leadingCoeff p)
unfold leadingCoeff
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]
⊢ coeff (map f p) (natDegree (map f p)) = ↑f (coeff p (natDegree p))
rw [coeff_map, natDegree_map_eq_of_injective hf p]