# Zulip Chat Archive

## Stream: Lean for teaching

### Topic: Resources for finite sets/types

#### Miguel Marco (Nov 29 2022 at 19:50):

Hi all,

I am giving an informal course of interactive proving with lean, for mathematics undergrad students.

I considered talking about finite sets and types, but haven't been able to think of a nice way to present them (mostly because the multiple incarnations of similar concepts: fintype, finset, finite and set.finite).

Do you know if there is some teaching material that covers that ?

#### Kevin Buzzard (Nov 29 2022 at 20:16):

yeah I tend to avoid finiteness. Did you talk about sets? If you have already explained sets then `finset`

is I guess the obvious next thing.

#### Patrick Massot (Nov 29 2022 at 21:21):

I certainly avoid finiteness in my teaching, but the goal is to teach math, not Lean.

#### Jeremy Avigad (Nov 30 2022 at 02:14):

Miguel, I am currently teaching a similar undergraduate class, and I have a bit of material that I used in lectures to give students some pointers about finite sets and structures. It's not really suitable for public consumption but I am planning to work it into another Mathematics in Lean chapter in the spring. In the meanwhile, I can share some of the material with you offline, if you would like.

#### Miguel Marco (Nov 30 2022 at 08:08):

Jeremy Avigad said:

Miguel, I am currently teaching a similar undergraduate class, and I have a bit of material that I used in lectures to give students some pointers about finite sets and structures. It's not really suitable for public consumption but I am planning to work it into another Mathematics in Lean chapter in the spring. In the meanwhile, I can share some of the material with you offline, if you would like.

That would be very helpful. Can you please email it to me?

#### Sina (Dec 06 2022 at 01:24):

@Jeremy Avigad I'd be interested too, since I have a student who is doing a final project on adjacency matrices of finite simple graphs, and so far my advice to him was to just do it for arbitrary types and avoid finiteness (as Kevin also said), but it would be nice to have some concrete finite types to reduce/eval some basic computation with adj matrices.

Last updated: Dec 20 2023 at 11:08 UTC