case zero
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
⊢ normalizedFactors (x ^ Nat.zero) = Nat.zero • normalizedFactors x

case succ
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
⊢ normalizedFactors (x ^ Nat.succ n) = Nat.succ n • normalizedFactors x
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ normalizedFactors (x ^ n) = n • normalizedFactors x
induction' n with n ih
case pos
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ Nat.succ n) = Nat.succ n • normalizedFactors x

case neg
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x ^ Nat.succ n) = Nat.succ n • normalizedFactors x
case succ
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
⊢ normalizedFactors (x ^ Nat.succ n) = Nat.succ n • normalizedFactors x
by_cases h0 : x = 0
no goals
case neg
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x ^ Nat.succ n) = Nat.succ n • normalizedFactors x
rw [pow_succ, succ_nsmul, normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]
no goals
case zero
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
⊢ normalizedFactors (x ^ Nat.zero) = Nat.zero • normalizedFactors x
simp
no goals
case pos
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ Nat.succ n) = Nat.succ n • normalizedFactors x
simp [h0, zero_pow n.succ_pos, smul_zero]