case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r ^ Nat.zero = ↑(monomial (n * Nat.zero)) (r ^ Nat.zero)

case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r ^ k = ↑(monomial (n * k)) (r ^ k)
⊢ ↑(monomial n) r ^ Nat.succ k = ↑(monomial (n * Nat.succ k)) (r ^ Nat.succ k)
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
⊢ ↑(monomial n) r ^ k = ↑(monomial (n * k)) (r ^ k)
induction' k with k ih
no goals
case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r ^ Nat.zero = ↑(monomial (n * Nat.zero)) (r ^ Nat.zero)
simp [pow_zero, monomial_zero_one]
no goals
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r ^ k = ↑(monomial (n * k)) (r ^ k)
⊢ ↑(monomial n) r ^ Nat.succ k = ↑(monomial (n * Nat.succ k)) (r ^ Nat.succ k)
simp [pow_succ, ih, monomial_mul_monomial, Nat.succ_eq_add_one, mul_add, add_comm]