Multiplicity in the naturals

Stream: Is there code for X?

[Bhavik Mehta]

Right now it seems that we have two ways of talking about the multiplicity of a prime in a natural: using multiplicity (via ring theory) or n.factors.count p. Is there a result linking the two values anywhere?

[Eric Rodriguez]

there's also padic_val_nat

[Eric Rodriguez]

There's also gonna be factorization: nat -> nat ->0 nat soon, (cc @Stuart Presnell ); I think we definitely need a unified API for this

[Yaël Dillies]

And there will soon be factorization

[Yaël Dillies]

Arf! Beat me to it

[Eric Rodriguez]

I suggeseted a sort of "elementary" definition in file#data/nat/mul_ind, I can work on it if people think it's a good idea to supersede all these...

[Bhavik Mehta]

Eric Rodriguez said:

There's also gonna be factorization: nat -> nat ->0 nat soon, (cc Stuart Presnell ); I think we definitely need a unified API for this

Isn't factorization just taking the list of factors as a multiset, then converting this to a finsupp?

[Bhavik Mehta]

And it seems that padic_val_nat is just a thin wrapper around multiplicity

[Bhavik Mehta]

Eric Rodriguez said:

There's also gonna be factorization: nat -> nat ->0 nat soon, (cc Stuart Presnell ); I think we definitely need a unified API for this

I'm not so sure we need an API to be honest, n.factors and multiplicity are pretty independently useful (the first when you want the list of prime factors and the second for general ring theory), it's just that when the two can be used to produce the same number, we should be able to show they're the same number and decide on a canonical way to talk about that number!

[Eric Rodriguez]

docs#padic_val_nat_eq_factors_count seems to be proved by hand, so it seems not

[Eric Rodriguez]

i guess there's now a proof with that .trans padic_val_nat eq multiplicity ..., but probably not the right approach

[Stuart Presnell]

Yeah, when I proposed factorization it was suggested that defining it as a finsupp would be useful since this makes that API available.

[Bhavik Mehta]

Hmm I see, thanks for pointing that one out! I think the best approach is to have a lemma at the end of data/nat/prime saying that the multiplicity and factor count coincide, and declaring that multiplicity should be used wherever possible (since it is defined for rings, not just for naturals.

[Bhavik Mehta]

In particular I'm suggesting deprecating lemmas like docs#nat.le_factors_count_mul_left in favour of multiplicity versions of themselves

[Stuart Presnell]

In a review a few days ago @Johan Commelin suggested generalising factorization to a unique factorization monoid that also has a normalization function.

[Bhavik Mehta]

I think that would be a good idea too, but perhaps orthogonal to this concern?

[Eric Rodriguez]

even for nat, multiplicity is a pain to work with because of docs#multiplicity.finite_nat_iff, and pretty much every theorem being about multiplicity.get ... or requiring a finite argument, which quickly becomes longwinded

[Bhavik Mehta]

Fair point. Do you think we should prefer the factors.count version then?

[Eric Rodriguez]

I think that seems reasonable, or factorization once it's done. I also quite like the padic_val_nat API so I could try port some things over to there eventually, things like docs#padic_val_nat.div are quite nice

[Eric Rodriguez]

(and docs#pow_succ_padic_val_nat_not_dvd, this is my favourite theorem)

[Bhavik Mehta]

Right, it looks like a good portion of those lemmas could be proved without mentioning padics and just live in data/nat/prime or something, and the padic version could be a one or two line corollary

[Stuart Presnell]

I think the initial PR setting up the basics of factorization (#10540) should be ready to merge now. As @Bhavik Mehta suggested I've added a TODO note indicating that we want to straighten out factors.count, padic_val_nat, multiplicity, and the material in data/pnat/factors.

[Stuart Presnell]

I also have #10850 which adds a few lemmas involving factorizations of coprime numbers, and #11167 which proves that we can evaluate a multiplicative function f n by evaluating f at p ^ k over the factorization of n.

[Bhavik Mehta]

Currently working on merging factors.count into factorization. It seems like we've agreed factorization should be the normal form (for multiplicity in the naturals), so I'm moving lemmas which talk about factors.count into factorization and stating them in terms of the latter.

[Bolton Bailey]

I've been working on PR #12301 to make factorization more computable. I'm currently on the path of redefining factorization in terms of padic_val_nat.
It strikes me as odd that padic_val_nat is defined in terms of padic_val_rat instead of the other way around: This way, to evaluate padic_val_nat, we first cast to a rational then take the multiplicity of both the numerator and denominator, then cast the result back to a nat from an int. The other way, we could just say padic_val_nat is the multiplicity as a total function, and padic_val_rat is the difference of the padic_val_nats of the abs of the numerator and denominator. Perhaps this could be switched?

[Bolton Bailey]

Plus we have a bunch of strange lemmas such as docs#padic_val_nat_def, which includes argument [fact p.prime] when all that's necessary is p \ne 0.

[Bolton Bailey]

I'm perhaps a bit uncomfortable calling this function padic_val_nat at all, since wikipedia tells me this is a concept that's only for primes.

[Johan Commelin]

Refactoring is fine, I guess. But have you considered using tactics for the computations? That will often be much faster than kernel computations.

[Mario Carneiro]

If there is a specific function on naturals you want computed, I can write a norm_num extension