Stream: math-comp users

Topic: ✔ Unicity of prime decomposition

Pierre-Yves Strub (May 31 2022 at 06:52):

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

Cyril Cohen (May 31 2022 at 09:33):

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`).

Pierre-Yves Strub (May 31 2022 at 09:36):

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

Cyril Cohen (May 31 2022 at 09:39):

Pierre-Yves Strub said:

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

I did not find it either!

Pierre-Yves Strub (May 31 2022 at 09:39):

Ok. Will do a PR later then.

Notification Bot (May 31 2022 at 09:39):

Pierre-Yves Strub has marked this topic as resolved.

Cyril Cohen (May 31 2022 at 09:42):

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

Pierre-Yves Strub (May 31 2022 at 09:42):

The main question is how to express it properly

Pierre-Yves Strub (May 31 2022 at 09:43):

I have several of them :)

s/is/are/

Pierre-Yves Strub (May 31 2022 at 09:44):

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}.
``````

Pierre-Yves Strub (May 31 2022 at 09:44):

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

Pierre-Yves Strub (May 31 2022 at 09:45):

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.
``````

Cyril Cohen (May 31 2022 at 09:47):

I had this one in mind:

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

Edited (fixed a typo)

Cyril Cohen (May 31 2022 at 09:48):

(unproven untested)

Pierre-Yves Strub (May 31 2022 at 09:48):

Yes, that's also a solution

Pierre-Yves Strub (May 31 2022 at 09:49):

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

Last updated: Jul 15 2024 at 21:02 UTC