R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : degree f ≠ 0
⊢ ∀ (x : R), IsUnit x → ¬↑C x = f
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : degree f ≠ 0
⊢ span {f} ≠ ⊤
simp_rw [Ne.def, span_singleton_eq_top, Polynomial.isUnit_iff, not_exists, not_and]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : IsUnit x
h : degree (↑C x) ≠ 0
⊢ False
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : degree f ≠ 0
⊢ ∀ (x : R), IsUnit x → ¬↑C x = f
rintro x hx rfl
no goals
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : IsUnit x
h : degree (↑C x) ≠ 0
⊢ False
exact h (degree_C hx.ne_zero)