R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
r : R
i : ℕ
✝ : Nontrivial R
⊢ leadingCoeff ((X + ↑C r) ^ i) = 1
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
r : R
i : ℕ
⊢ leadingCoeff ((X + ↑C r) ^ i) = 1
nontriviality
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
r : R
i : ℕ
✝ : Nontrivial R
⊢ leadingCoeff ((X + ↑C r) ^ i) = 1
rw [leadingCoeff_pow'] <;> simp