no goals
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
n : ℕ
hp0 : p = 0
hn0 : n = 0
⊢ natDegree (p ^ n) = n * natDegree p
simp [hp0, hn0]
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
n : ℕ
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree 0 = n * natDegree 0
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
n : ℕ
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree (p ^ n) = n * natDegree p
rw [hp0, zero_pow (Nat.pos_of_ne_zero hn0)]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
n : ℕ
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree 0 = n * natDegree 0
simp
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
n : ℕ
hp0 : ¬p = 0
⊢ ¬p ^ n = 0
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
n : ℕ
hp0 : ¬p = 0
⊢ leadingCoeff p ^ n ≠ 0
rw [← leadingCoeff_pow, Ne.def, leadingCoeff_eq_zero]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
n : ℕ
hp0 : ¬p = 0
⊢ ¬p ^ n = 0
exact pow_ne_zero _ hp0