R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
✝ : Nontrivial R
⊢ leadingCoeff (X ^ n + ↑C r) = 1
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
⊢ leadingCoeff (X ^ n + ↑C r) = 1
nontriviality R
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
✝ : Nontrivial R
⊢ leadingCoeff (X ^ n + ↑C r) = 1
rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
  if_neg (pos_iff_ne_zero.mp hn), add_zero]