case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
⊢ coeff (p ^ Nat.zero) (n * Nat.zero) = coeff p n ^ Nat.zero

case succ
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (n * m) = coeff p n ^ m
⊢ coeff (p ^ Nat.succ m) (n * Nat.succ m) = coeff p n ^ Nat.succ m
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
⊢ coeff (p ^ m) (n * m) = coeff p n ^ m
induction' m with m hm
no goals
case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
⊢ coeff (p ^ Nat.zero) (n * Nat.zero) = coeff p n ^ Nat.zero
simp
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (n * m) = coeff p n ^ m
⊢ natDegree (p ^ m) ≤ n * m
case succ
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (n * m) = coeff p n ^ m
⊢ coeff (p ^ Nat.succ m) (n * Nat.succ m) = coeff p n ^ Nat.succ m
rw [pow_succ', pow_succ', ← hm, Nat.mul_succ, coeff_mul_of_natDegree_le _ pn]
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (n * m) = coeff p n ^ m
⊢ m * natDegree p ≤ m * n
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (n * m) = coeff p n ^ m
⊢ natDegree (p ^ m) ≤ n * m
refine' natDegree_pow_le.trans (le_trans _ (mul_comm _ _).le)
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (n * m) = coeff p n ^ m
⊢ m * natDegree p ≤ m * n
exact mul_le_mul_of_nonneg_left pn m.zero_le