## Stream: new members

### Topic: How to get Subtypes to inherit typeclasses

#### Jem Bishop (Nov 05 2020 at 16:31):

Hi! I want to create a subtype of the natural numbers less than or equal to 5. With
def House := {n : ℕ // n ≤ 5}
this seems to lose all the typeclass instances the natural numbers have, (I can't add or use = with nats) ! How do I get them for this subtype? Thanks!

#### Johan Commelin (Nov 05 2020 at 16:33):

@Jem Bishop What is 4 + 4 in this type?

#### Johan Commelin (Nov 05 2020 at 16:33):

Note that mathlib has fin 6 and zmod 6 which are two types that have the same definition as House but are equipped with a bunch of typeclass instances.

#### Jem Bishop (Nov 05 2020 at 16:35):

I see, thanks for your help!

#### Jem Bishop (Nov 05 2020 at 16:40):

In this case I would like 4 + 4 = 5, so I guess I would create these instances for add on fin manually

#### Yury G. Kudryashov (Nov 05 2020 at 21:15):

(deleted)

Last updated: May 11 2021 at 13:22 UTC