case zero
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ roots (p ^ Nat.zero) = Nat.zero • roots p

case succ
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
n : ℕ
ihn : roots (p ^ n) = n • roots p
⊢ roots (p ^ Nat.succ n) = Nat.succ n • roots p
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
n : ℕ
⊢ roots (p ^ n) = n • roots p
induction' n with n ihn
no goals
case zero
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ roots (p ^ Nat.zero) = Nat.zero • roots p
rw [pow_zero, roots_one, Nat.zero_eq, zero_smul, empty_eq_zero]
case succ.inl
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
ihn : roots (0 ^ n) = n • roots 0
⊢ roots (0 ^ Nat.succ n) = Nat.succ n • roots 0

case succ.inr
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
n : ℕ
ihn : roots (p ^ n) = n • roots p
hp : p ≠ 0
⊢ roots (p ^ Nat.succ n) = Nat.succ n • roots p
case succ
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
n : ℕ
ihn : roots (p ^ n) = n • roots p
⊢ roots (p ^ Nat.succ n) = Nat.succ n • roots p
rcases eq_or_ne p 0 with (rfl | hp)
no goals
case succ.inl
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
ihn : roots (0 ^ n) = n • roots 0
⊢ roots (0 ^ Nat.succ n) = Nat.succ n • roots 0
rw [zero_pow n.succ_pos, roots_zero, smul_zero]
no goals
case succ.inr
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
n : ℕ
ihn : roots (p ^ n) = n • roots p
hp : p ≠ 0
⊢ roots (p ^ Nat.succ n) = Nat.succ n • roots p
rw [pow_succ', roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, Nat.succ_eq_add_one,
  add_smul, one_smul]