The product of pairwise nonassociated elements is injective.

Stream: Is there code for X?

[metakuntyyy]

I need something like this.

import Mathlib

theorem associates_test  {a c: Type*} (f : a → c)
 [CancelCommMonoidWithZero c] [UniqueFactorizationMonoid c]
 (h2: ∀ i: a, ∀ j : a, Associated (f i) (f j) → i = j )
  {p q : Multiset a}
  (h : (Multiset.map f p).prod =(Multiset.map f q).prod) : p = q := by sorry

The context. Given $a=\{0,...,l\}$ I need to show that the product of polynomials $(x+i)^{k(i)}$ is distinct.

The proof idea is by contradiction. Assume $p\neq q$, then there exists an $\alpha \in a$ such that the indices of $p(a)$ and $q(a)$ are different. Assume w.l.o.g that the index i of $p(a)$ is strictly bigger that the index of $q(a)$, then $(f a)^i$ divides (Multiset.map f p).prod but not (Multiset.map f q).prod, this concludes the proof. We use the assumption h2 to split the product into $x = a$ and $x \neq a$, if (f a) divides the product, it must divide the first factor, as the second factor contains only non-associated elements to (f a).

[metakuntyyy]

Note that you can weaken the hypothesis h by replacing the equals with the associated relation. I want to show that the product of pairwise non-associated elements is injective.

[Kenny Lau]

import Mathlib

theorem associates_test  {a c: Type*} (f : a → c)
 [CancelCommMonoidWithZero c] [UniqueFactorizationMonoid c]
 (h2: ∀ i: a, ∀ j : a, Associated (f i) (f j) → i = j )
  {p q : Multiset a}
  (h : (Multiset.map f p).prod =(Multiset.map f q).prod) : p = q := by sorry

example : False :=
  absurd (associates_test (a := Fin 4) (c := ℕ) ![2, 5, 6, 15] (by decide)
    (p := {0, 3}) (q := {1, 2}) rfl) (by decide)

2 * 15 = 5 * 6

[metakuntyyy]

Let me try to refine my statement.

[Kenny Lau]

Anyway, the theorem you're searching for is prime_factors_unique:

theorem prime_factors_unique [CancelCommMonoidWithZero α] :
    ∀ {f g : Multiset α},
      (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g

[metakuntyyy]

Yes, thank you very much.

[metakuntyyy]

I likely don't need the full strength of the theorem. I'll try to write down a specialized theorem that has easier hypotheses.

[metakuntyyy]

Second try, hopefully I got it right this time.

import Mathlib

theorem prime_factors_unique2 {α x: Type*} [CancelCommMonoidWithZero α]
[UniqueFactorizationMonoid α] (x: Set α) (hpr: ∀ e ∈ x, Prime e)
  {f g : Multiset {e| e∈ x }}
  (heq: Multiset.map (fun (x:{e| e∈ x })=>x.val) f = Multiset.map (fun (x:{e| e∈ x })=>x.val) g)
  (h: ∀ i ∈ x, ∀ j∈ x, Associated i j → i =j) :
    f=g  := sorry

[metakuntyyy]

I want to use a set x, in my case the linear factors (x-1),...(x-n), show that they are pairwise associate to conclude that the mapping of functions g: (1,...n) -> Nat, that maps g to the product of powers of (x-_) is injective.

[metakuntyyy]

Is this an easy corollary?