Pierre-Yves Strub said:

Hi. I cannot find anything that is close to state the unicity of prime decomposition.

I don't know how to do otherwise than using `logn`

or `partn`

(notation `n`_pi`

).

Well, doing it is ok. But you confirm that nothing exists in the stdlib?

Pierre-Yves Strub said:

Well, doing it is ok. But you confirm that nothing exists in the stdlib?

I did not find it either!

Ok. Will do a PR later then.

Pierre-Yves Strub has marked this topic as resolved.

I think the basic blocks to prove it should be `prime_decompE`

and `lognM`

.

Already have a proof.

The main question is how to express it properly

what is your statement?

I have several of them :)

s/is/are/

But the most general is something in the line:

```
(ps : seq nat) (F G : nat -> nat) :
uniq ps
-> {in ps, forall p, prime p}
-> \prod_(p <- ps) p ^ (F p) = \prod_(p <- ps) p ^ (G p)
-> {in ps, forall p, F p = G p}.
```

(Proof not finished, so maybe I have a typo somewhere in the statement :) )

Otherwise, I have a more specific one:

```
Definition is_canon_prime_decomp_for (n : nat) (pes : seq (nat * nat)) :=
[/\ {in pes, forall pe, [/\ prime pe.1, 0 < pe.2 & pe.1 ^ pe.2 %| n]}
, sorted ltn (unzip1 pes)
& n = \prod_(pe <- pes) pe.1 ^ pe.2 ].
Lemma uniq_canon_prime_decomp (n : nat) (pes qes : seq (nat * nat)) :
is_canon_prime_decomp_for n pes
-> is_canon_prime_decomp_for n qes
-> pes = qes.
```

So choose your poison

I had this one in mind:

```
Lemma perm_prime_decomp (s : seq (nat * nat)) :
uniq (map fst s) -> all prime (map fst s) -> all (gtn 0) (map snd s) ->
perm_eq (prime_decomp (\prod_(x <- s) x.1 ^ x.2)) s.
```

(unproved untested)

Yes, that's also a solution

I'll take it because I don't have a strong opinion on this.

Last updated: Feb 08 2023 at 08:02 UTC