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