R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
this : leadingCoeff p ≠ 0
⊢ ↑(normUnit p) = ↑C (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]
hp : p ≠ 0
⊢ ↑(normUnit p) = ↑C (leadingCoeff p)⁻¹
have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp
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]
hp : p ≠ 0
this : leadingCoeff p ≠ 0
⊢ ↑(normUnit p) = ↑C (leadingCoeff p)⁻¹
simp [CommGroupWithZero.coe_normUnit _ this]