## Stream: maths

### Topic: trivial group

#### Kevin Buzzard (Apr 20 2021 at 15:46):

I want to say that an add_comm_group is the trivial group $\{0\}$. Should I use subsingleton or unique?

#### Anne Baanen (Apr 20 2021 at 15:58):

There is an instance docs#unique.subsingleton, right? Then unique is just strictly more useful.

#### Gabriel Ebner (Apr 20 2021 at 16:00):

If it's an assumption to a lemma, then I'd use subsingleton.

#### Sebastien Gouezel (Apr 20 2021 at 16:08):

The great advantage of subsingleton is that it has no data in it, contrary to unique.

#### Eric Wieser (Apr 20 2021 at 16:14):

Although if you have [add_comm_group A] [unique A], chances are the data in unique is defeq to the zero in add_comm_group anyway

#### Eric Wieser (Apr 20 2021 at 16:14):

So the presence / absence of data is unlikely to matter

#### Kevin Buzzard (Apr 20 2021 at 16:20):

It's the conclusion of a lemma. Oh, if unique isn't a prop, forget it :-)

#### Kevin Buzzard (Apr 20 2021 at 16:20):

who knows what the element is

#### Gabriel Ebner (Apr 20 2021 at 16:22):

Eric Wieser said:

Although if you have [add_comm_group A] [unique A], chances are the data in unique is defeq to the zero in add_comm_group anyway

That's exactly the situation where they are not defeq:

example {α} [add_comm_group α] [unique α] : default α = 0 := rfl -- fails


#### Nick Scheel (Apr 20 2021 at 16:59):

I suspect Eric meant that for a concrete A that satisfies those constraints, the two definitions will probably agree, but obviously not when A is unknown, as you showed.

#### Kevin Buzzard (Apr 20 2021 at 17:00):

It hadn't occurred to me that unique wasn't a Prop; in my use case I want a Prop. Do we have propositional uniqueness? Not that it matters urgently, I've gone with subsingleton now.

#### Anne Baanen (Apr 20 2021 at 17:16):

unique α is a subsingleton for what it's worth, but yeah, if you need a Prop then subsingleton is the way to go

Last updated: Jun 17 2021 at 16:20 UTC