integer valuation

Stream: Is there code for X?

[Edison Xie]

I've noticed there is Valuation and there is ValuationRing in mathlib4, however is there anything for integer valuation?
And also the definition I know is a function f : K -> (WithTop ℤ) where f(ab) = f(a) + f(b) and also f(a) = ⊤ ↔ a = 0, apparently things work differently in mathlib and I'll appreciate if someone can let me know what should I do to define such a valuation.

[Luigi Massacci]

You want docs#AddValuation

[Yaël Dillies]

That would a docs#AddValuation

[Luigi Massacci]

Specifically, docs#AddValuation.of is probably what you would be most comfortable with

[Edison Xie]

thanks!

[Notification Bot]

Edison Xie has marked this topic as resolved.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Filippo A. E. Nuccio]

Let me stress at any rate the we probably prefer to only stick to multiplicative ones, even if this diverges a bit from the classical math literature.

[Edison Xie]

Why is that the case :((

[Andrew Yang]

docs#AddValuation is also not what you would find in the literature. What you are thinking is probably $v(ab) = v(a) + v(b)$ which sends a multiplicative group to an additive group. This is not supported in mathlib so we either need to multiplicativise the range or additivise the domain. If we go for the latter we would want $v(0) = \infty$ but we do not have the theory of "add-group-with-infinity" in mathlib so the former is the sensible choice.

[Luigi Massacci]

Now I’m confused. How is docs#AddValuation not $v(ab) = v(a) + v(b)$ , $v(0) = \infty$?

[Andrew Yang]

Oh it is. Sorry I was confused.

[Kevin Buzzard]

But there's definitely more API in general for "things with 0" than "things with infinity" eg ring works better