α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k =
    match some (replicate k { val := p, property := hp }) with
    | none => 0
    | some s => prod (map Subtype.val s)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ FactorSet.prod (factors (p ^ k)) = FactorSet.prod (some (replicate k { val := p, property := hp }))
rw [Associates.factors_prod, FactorSet.prod]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k = prod (map Subtype.val (replicate k { val := p, property := hp }))
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k =
    match some (replicate k { val := p, property := hp }) with
    | none => 0
    | some s => prod (map Subtype.val s)
dsimp
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k = prod (map Subtype.val (replicate k { val := p, property := hp }))
rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk]