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

case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : X ^ n = ↑(monomial n) 1
⊢ X ^ Nat.succ n = ↑(monomial (Nat.succ n)) 1
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ X ^ n = ↑(monomial n) 1
induction' n with n hn
no goals
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X ^ Nat.zero = ↑(monomial Nat.zero) 1
rw [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 : ℕ
hn : X ^ n = ↑(monomial n) 1
⊢ X ^ Nat.succ n = ↑(monomial (Nat.succ n)) 1
rw [pow_succ', hn, X, monomial_mul_monomial, one_mul]