α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ p ^ ZeroHom.toFun (↑Multiset.card) (normalizedFactors r) ~ᵤ r
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ ∃ i, p ^ i ~ᵤ r
use Multiset.card.toFun (normalizedFactors r)
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : Multiset.prod (normalizedFactors r) ~ᵤ r
⊢ p ^ ZeroHom.toFun (↑Multiset.card) (normalizedFactors r) ~ᵤ r
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ p ^ ZeroHom.toFun (↑Multiset.card) (normalizedFactors r) ~ᵤ r
have := UniqueFactorizationMonoid.normalizedFactors_prod hr
no goals
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : Multiset.prod (normalizedFactors r) ~ᵤ r
⊢ p ^ ZeroHom.toFun (↑Multiset.card) (normalizedFactors r) ~ᵤ r
rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this