R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
✝ : Nontrivial R
⊢ Monic (trinomial k m n u v 1)
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ Monic (trinomial k m n u v 1)
nontriviality R
no goals
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
✝ : Nontrivial R
⊢ Monic (trinomial k m n u v 1)
exact trinomial_leadingCoeff hkm hmn one_ne_zero