case a
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]
hp : Monic (map f p)
⊢ ↑f (leadingCoeff p) = ↑f 1
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]
hp : Monic (map f p)
⊢ Monic p
apply hf
no goals
case a
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]
hp : Monic (map f p)
⊢ ↑f (leadingCoeff p) = ↑f 1
rw [← leadingCoeff_of_injective hf, hp.leadingCoeff, f.map_one]