case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
⊢ count p (factors (a ^ Nat.zero)) = Nat.zero * count p (factors a)

case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : count p (factors (a ^ n)) = n * count p (factors a)
⊢ count p (factors (a ^ Nat.succ n)) = Nat.succ n * count p (factors a)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ count p (factors (a ^ k)) = k * count p (factors a)
induction' k with n h
no goals
case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
⊢ count p (factors (a ^ Nat.zero)) = Nat.zero * count p (factors a)
rw [pow_zero, factors_one, Nat.zero_eq, zero_mul, count_zero hp]
case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : count p (factors (a ^ n)) = n * count p (factors a)
⊢ count p (factors a) + n * count p (factors a) = (n + 1) * count p (factors a)
case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : count p (factors (a ^ n)) = n * count p (factors a)
⊢ count p (factors (a ^ Nat.succ n)) = Nat.succ n * count p (factors a)
rw [pow_succ, count_mul ha (pow_ne_zero _ ha) hp, h, Nat.succ_eq_add_one]
no goals
case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : count p (factors (a ^ n)) = n * count p (factors a)
⊢ count p (factors a) + n * count p (factors a) = (n + 1) * count p (factors a)
ring