# Zulip Chat Archive

## Stream: general

### Topic: noncomputable card

#### Kevin Buzzard (May 03 2020 at 12:24):

I'm going to have a summer student working with me on group theory and I wondered whether Sylow 2 and 3 was accessible to them. Talking to @Chris Hughes he seemed to think that a useful prerequisite would be a noncomputable `card`

function which sent infinite types to 0, and claimed that this was @Mario Carneiro 's idea. Does this sound like a sensible thing? I guess that if I were to write it I'd do it in June, because I'd need it by July. I already have bundled normal subgroups and adding metric space examples to Patrick's tutorial project on my Lean pile, plus two more grant applications, so it's unlikely it will happen before then, but I thought I'd run it past the community in case anyone had any comments or tips.

#### Mario Carneiro (May 03 2020 at 12:33):

It should be easy work

#### Mario Carneiro (May 03 2020 at 12:34):

you will have a lot of finiteness assumptions though in the theorems, because that `0`

garbage case will mess up the algebra

#### Reid Barton (May 03 2020 at 12:40):

What about an `enat`

-valued `card`

?

#### Mario Carneiro (May 03 2020 at 12:54):

I like that version the best if we ignore typing problems

#### Mario Carneiro (May 03 2020 at 12:54):

it's not clear to me how important it is that the value be a nat

#### Kevin Buzzard (May 03 2020 at 12:54):

@Chris Hughes would an `enat`

-valued version be good enough for applications to Sylow 2/3?

#### Mario Carneiro (May 03 2020 at 12:54):

Is there a `enat.to_nat`

function? We could compose through that when necessary

#### Mario Carneiro (May 03 2020 at 12:55):

You can still use the enat version for a predicate like `card A = enat.of_nat n`

#### Mario Carneiro (May 03 2020 at 12:56):

which asserts both finiteness and a particular cardinality without a `fintype`

assumption

#### Chris Hughes (May 03 2020 at 12:56):

enat would be hideous for group theory because you're always raising to the power of the cardinality, and multiplying the cardinality etc.

#### Mario Carneiro (May 03 2020 at 12:57):

would those theorems work with a predicate like I gave?

#### Mario Carneiro (May 03 2020 at 12:57):

you have an assumption `card A = (n : nat)`

and then use `n`

in the theorem

#### Chris Hughes (May 03 2020 at 13:11):

Probably they would. Multiplicity was really bad, because I didn't state theorems like that.

#### Johan Commelin (May 03 2020 at 13:16):

Why would you need an `enat`

valued `card`

for such predicates?

#### Johan Commelin (May 03 2020 at 13:16):

Wouldn't the cardinal-valued version suffice?

#### Mario Carneiro (May 03 2020 at 13:24):

You don't need to import `set_theory.cardinal`

to define the `enat`

version

#### Chris Hughes (May 03 2020 at 13:26):

Are imports really that bad?

#### Jeremy Avigad (May 04 2020 at 01:37):

In Lean 2, we had a nonconstructive cast from `set`

to `finset`

which mapped any infinite set to the empty set. So we had `set.card s = finset.card (s.to_finset)`

. The cardinality of the empty set still comes out to zero, and it is easy to translate `finset`

theorems (e.g. about `card`

and `sum`

) to `set`

theorems.

The advantage to having `card`

and `sum`

map infinite sets to `0`

is that lots of identities hold without preconditions. It makes it much more convenient to work with them. Isabelle follows that approach as well.

Last updated: May 13 2021 at 23:16 UTC