R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
u : R[X]ˣ
⊢ coeff (↑u) (natDegree ↑u) ≠ 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
u : R[X]ˣ
⊢ coeff (↑u) 0 ≠ 0
conv in 0 => rw [← natDegree_coe_units u]
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
u : R[X]ˣ
⊢ ¬↑u = 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
u : R[X]ˣ
⊢ coeff (↑u) (natDegree ↑u) ≠ 0
rw [← leadingCoeff, Ne.def, leadingCoeff_eq_zero]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
u : R[X]ˣ
⊢ ¬↑u = 0
exact Units.ne_zero _