Divisibility to adic valuation

Stream: Is there code for X?

[Yaël Dillies]

Where is the fact that a divides b iff the adic valuations of a are smaller than the adic valuations of b? I guess the correct generality for that should be a UFD, but I'm happy to use ℕ-specific stuff. Also, I don't know what the correct thing to use.

[Kevin Buzzard]

There are about 37 different adic valuations

[Yaël Dillies]

Yeah that's what I was about to say :rofl:

[Yaël Dillies]

Why is that so?

[Yaël Dillies]

I list multiplicity, padic_val_nat, factor_multiset. factor_multiset isn't used at all, but I can't tell for the others.

[Kevin Buzzard]

padic_val_nat was perhaps an auxiliary function developed for the p-adic numbers and introduced before we had a general multiplicity function for rings

[Yaël Dillies]

Do we really not have anything like that?

[Kevin Buzzard]

The other issue is what to do with 0 -- this is constantly a problem with functions v satisfying v(ab)=v(a)+v(b) like valuations or degree of a polynomial over a field, which want to send 0 to +infty.