Multipliable of padicNorm

Stream: new members

[Sophia Rodriguez]

Hi all! do we have

Multipliable fun (p : Nat.Primes) ↦ padicNorm (↑p) x

(x is rational)? I am really confused by Multiset and List involved here. Like, since the padicNorm is 1 for any p that is big enough, so I want a Multiset of Nat.Primes for all primes less or equal to a given number (sth like {p : Nat.Primes // p.val ≤ m}), but I failed to construct it.

[Aaron Liu]

docs#Nat.primesBelow is the primes strictly below a number

[Sophia Rodriguez]

Thanks! Nat.primesBelow is mathematically the thing I want. But it is a Finset of ℕ, can I coercion it into a Finset of Nat.Primes?

[Aaron Liu]

Why do you want to use Nat.Primes?

[Sophia Rodriguez]

cause I want to do tprod throughout prime numbers, something like

∏' p : Nat.Primes, padicNorm p x = |x|⁻¹

[Aaron Liu]

You can use docs#Finset.attach and docs#Finset.map to make it into a Finset Nat.Primes.

[Sophia Rodriguez]

It works! thanks