Stream: math-comp users

Topic: ✔ Unicity of prime decomposition


view this post on Zulip 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).

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:36):

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

view this post on Zulip 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!

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:39):

Ok. Will do a PR later then.

view this post on Zulip Notification Bot (May 31 2022 at 09:39):

Pierre-Yves Strub has marked this topic as resolved.

view this post on Zulip Cyril Cohen (May 31 2022 at 09:42):

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

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:42):

Already have a proof.

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:42):

The main question is how to express it properly

view this post on Zulip Cyril Cohen (May 31 2022 at 09:43):

what is your statement?

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:43):

I have several of them :)

view this post on Zulip Cyril Cohen (May 31 2022 at 09:44):

s/is/are/

view this post on Zulip 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}.

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:44):

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

view this post on Zulip 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.

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:45):

So choose your poison

view this post on Zulip 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 (gtn 0) (map snd s) ->
  perm_eq (prime_decomp (\prod_(x <- s) x.1 ^ x.2)) s.

view this post on Zulip Cyril Cohen (May 31 2022 at 09:48):

(unproved untested)

view this post on Zulip Pierre-Yves Strub (May 31 2022 at 09:48):

Yes, that's also a solution

view this post on Zulip 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: Feb 08 2023 at 08:02 UTC