R : Type u_1
S : Type ?u.564413
F : Type ?u.564416
K : Type ?u.564419
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
✝ : Nontrivial R
⊢ Monic (toPoly P)
R : Type u_1
S : Type ?u.564413
F : Type ?u.564416
K : Type ?u.564419
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
⊢ Monic (toPoly P)
nontriviality R
no goals
R : Type u_1
S : Type ?u.564413
F : Type ?u.564416
K : Type ?u.564419
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
✝ : Nontrivial R
⊢ Monic (toPoly P)
rw [Monic, leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero), hc]