R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.648061
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
⊢ leadingCoeff p = 1
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.648061
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
⊢ Monic p
unfold Monic
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.648061
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
✝ : Nontrivial R
⊢ leadingCoeff p = 1
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.648061
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
⊢ leadingCoeff p = 1
nontriviality
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.648061
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
✝ : Nontrivial R
⊢ coeff p n ≠ 0
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.648061
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
✝ : Nontrivial R
⊢ leadingCoeff p = 1
refine' (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn _).trans p1
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.648061
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
✝ : Nontrivial R
⊢ coeff p n ≠ 0
exact ne_of_eq_of_ne p1 one_ne_zero