R : Type u_1
S : Type ?u.558294
F : Type ?u.558297
K : Type ?u.558300
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 1
✝ : Nontrivial R
⊢ Monic (toPoly P)
R : Type u_1
S : Type ?u.558294
F : Type ?u.558297
K : Type ?u.558300
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 1
⊢ Monic (toPoly P)
nontriviality R
no goals
R : Type u_1
S : Type ?u.558294
F : Type ?u.558297
K : Type ?u.558300
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 1
✝ : Nontrivial R
⊢ Monic (toPoly P)
rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]