## 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: May 15 2021 at 23:13 UTC