no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : p = 0
hn0 : n = 0
⊢ natDegree (p ^ n) = n * natDegree p
simp [*]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree 0 = n * natDegree 0
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
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
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree 0 = n * natDegree 0
simp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : leadingCoeff p ^ n ≠ 0
⊢ False
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
⊢ False
have h1 := h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : 0 ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : leadingCoeff p ^ n ≠ 0
⊢ False
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : leadingCoeff p ^ n ≠ 0
⊢ False
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : 0 ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : leadingCoeff p ^ n ≠ 0
⊢ False
exact h rfl
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ ↑(n • natDegree p) = ↑(n * natDegree p)
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ ↑(natDegree (p ^ n)) = ↑(n * natDegree p)
rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0,
    Nat.cast_withBot, ← WithBot.coe_nsmul, ← Nat.cast_withBot]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.688771
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ ↑(n • natDegree p) = ↑(n * natDegree p)
simp