R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + ↑C (-a) ≠ 0
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n - ↑C a ≠ 0
rw [sub_eq_add_neg, ← map_neg C a]
no goals
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + ↑C (-a) ≠ 0
exact X_pow_add_C_ne_zero hn _