## Stream: maths

### Topic: fincard and cardinal.to_nat

#### Aaron Anderson (Feb 18 2021 at 04:04):

On branch#cardinal_to_nat, I've added a function cardinal.to_nat and used it to make a function fincard that can give a N-valued cardinality for any type. This is the same construction used in the linear algebra library to define findim.

#### Aaron Anderson (Feb 18 2021 at 04:05):

If people think this is a good idea, I will adapt some more of the API for a similar fincard function used in this project: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/finsum/basic.lean

and then PR it.

#### Aaron Anderson (Feb 18 2021 at 04:07):

I also think it'd be useful to add an enat version, if only to be able to state things in a way that doesn't wig out people who intuitively don't want the cardinality of an infinite set to be 0.

#### Aaron Anderson (Feb 18 2021 at 04:07):

Obviously the first function would be named cardinal.to_enat, but what should the extended version of fincard be called?

#### Johan Commelin (Feb 18 2021 at 04:25):

This sounds like a very good idea. There has been talk about fincard for a long time on zulip, and I'm glad someone is actually picking it up.

#### Aaron Anderson (Feb 18 2021 at 06:04):

If I move fincard to a separate file, should it be under data? set_theory?

#### Johan Commelin (Feb 18 2021 at 06:22):

data/fintype/card.lean currently contains stuff that doesn't have to do anything with card at all :frown: :head_bandage: otherwise that would be a natural place, I guess

#### Johan Commelin (Feb 18 2021 at 06:22):

set_theory (to me) is about ZFC specific stuff

#### Johan Commelin (Feb 18 2021 at 06:22):

data sounds good to me

#### Kevin Buzzard (Feb 18 2021 at 07:54):

A new fincard file would surely be fine, is there ever an argument against adding a new file with a descriptive name?

#### Jason KY. (Feb 18 2021 at 10:39):

Aaron Anderson said:

If people think this is a good idea, I will adapt some more of the API for a similar fincard function used in this project: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/finsum/basic.lean

There is some APIs for this on the fincard branch of mathlib which can be useful I hope. However, it's mostly for finsum so I'm not sure if its helpful after all
https://github.com/leanprover-community/mathlib/blob/fincard/src/data/fincard.lean

#### Aaron Anderson (Mar 01 2021 at 20:09):

#6494

Last updated: May 10 2021 at 08:14 UTC