Zulip Chat Archive

Stream: general

Topic: finset of divisors of pnat


view this post on Zulip 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:

view this post on Zulip Johan Commelin (May 15 2019 at 18:18):

And finset.range lives in finset nat.

view this post on Zulip Chris Hughes (May 15 2019 at 18:20):

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

view this post on Zulip Chris Hughes (May 15 2019 at 18:21):

I guess you want a version of range for pnat?

view this post on Zulip Chris Hughes (May 15 2019 at 18:22):

I used this finset in data.nat.totient

view this post on Zulip Johan Commelin (May 15 2019 at 18:29):

Did you give it a name?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Chris Hughes (May 15 2019 at 18:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 16 2019 at 02:20):

It does let you make a finset though

view this post on Zulip Johan Commelin (May 16 2019 at 05:51):

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


Last updated: May 15 2021 at 23:13 UTC