Zulip Chat Archive

Stream: general

Topic: finset of divisors of pnat


Johan Commelin (May 15 2019 at 18:18):

I've got a n : pnat and I want the finset pnat consisting of the divisors of n. I've already made an instance has_dvd pnat (woot!). What is now the cleanest way to get this finset?
Of course... ... { d | d \| n } will not work... ... ... :expressionless:

Johan Commelin (May 15 2019 at 18:18):

And finset.range lives in finset nat.

Chris Hughes (May 15 2019 at 18:20):

(range (n : nat).succ).filter (\| n) gives the correct finset in nat.

Chris Hughes (May 15 2019 at 18:21):

I guess you want a version of range for pnat?

Chris Hughes (May 15 2019 at 18:22):

I used this finset in data.nat.totient

Johan Commelin (May 15 2019 at 18:29):

Did you give it a name?

Johan Commelin (May 15 2019 at 18:31):

I really don't like the idea of duplicating all the range and Ico, etc... definitions and all their lemmas for nat and pnat and int... etc...

Johan Commelin (May 15 2019 at 18:35):

I think I might do

def pnat.divisors (n : ℕ+) : set ℕ+ :=
{d | d  n}

and then provide a fintype instance

Chris Hughes (May 15 2019 at 18:50):

It depends what you want to do with it, but you almost certainly want a finset.

Scott Morrison (May 15 2019 at 21:27):

Perhaps a good project would be to make list.range, list.Ico, and finset.Ico type polymorphic.

Scott Morrison (May 15 2019 at 21:28):

I'm not sure we yet have an appropriate typeclass describing the behaviour of succ that makes this possible in nat, pnat, int, and friends.

Chris Hughes (May 15 2019 at 21:32):

I guess it's just an ordered type where intervals are always finite. The order on finset has this property as well.

Scott Morrison (May 16 2019 at 02:17):

Well, you need some mechanism to actually list the elements in order, don't you? Merely asserting there's an order, and intervals are finite, doesn't let you make a list. I was imagining some sort of has_succ typeclass.

Mario Carneiro (May 16 2019 at 02:20):

It does let you make a finset though

Johan Commelin (May 16 2019 at 05:51):

There was some talk about enumerable on this chat, some time ago.


Last updated: Dec 20 2023 at 11:08 UTC