R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp0 : IsUnit (leadingCoeff p)
⊢ Monic (↑normalize p)
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp0 : p ≠ 0
⊢ Monic (↑normalize p)
rw [Ne.def, ← leadingCoeff_eq_zero, ← Ne.def, ← isUnit_iff_ne_zero] at hp0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp0 : IsUnit (leadingCoeff p)
⊢ IsUnit (leadingCoeff p)
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp0 : IsUnit (leadingCoeff p)
⊢ Monic (↑normalize p)
rw [Monic, leadingCoeff_normalize, normalize_eq_one]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp0 : IsUnit (leadingCoeff p)
⊢ IsUnit (leadingCoeff p)
apply hp0