## Stream: general

### Topic: group.inhabited

#### Kenny Lau (Apr 21 2018 at 01:44):

Should we show that every group is inhabited? Should we generalize it to has_one and has_zero? Which one will ring choose?

#### Mario Carneiro (Apr 21 2018 at 02:03):

I'm inclined to say no. inhabited is more of a programming notion, a way to acquire a "default" value when it doesn't matter what value is picked. The value has no semantic meaning, so it doesn't matter if one or zero is picked. But I don't think that a typeclass search for inhabited should go on an algebraic quest to prove that it's an R-module just because that implies it's inhabited. It would be better to have the types themselves register as inhabited, to keep it simple.

#### Kenny Lau (Apr 21 2018 at 02:04):

ok

Last updated: May 11 2021 at 12:15 UTC