α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
✝ : Nontrivial α
⊢ FactorSet.prod (factors a ⊔ factors b) * FactorSet.prod (factors a ⊓ factors b) = a * b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
⊢ FactorSet.prod (factors a ⊔ factors b) * FactorSet.prod (factors a ⊓ factors b) = a * b
nontriviality α
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
✝ : Nontrivial α
⊢ factors (FactorSet.prod (factors a ⊔ factors b) * FactorSet.prod (factors a ⊓ factors b)) = factors (a * b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
✝ : Nontrivial α
⊢ FactorSet.prod (factors a ⊔ factors b) * FactorSet.prod (factors a ⊓ factors b) = a * b
refine' eq_of_factors_eq_factors _
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
✝ : Nontrivial α
⊢ factors (FactorSet.prod (factors a ⊔ factors b) * FactorSet.prod (factors a ⊓ factors b)) = factors (a * b)
rw [← prod_add, prod_factors, factors_mul, FactorSet.sup_add_inf_eq_add]