trivial group

Stream: maths

[Kevin Buzzard]

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

[Anne Baanen]

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

[Gabriel Ebner]

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

[Sebastien Gouezel]

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

[Eric Wieser]

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]

So the presence / absence of data is unlikely to matter

[Kevin Buzzard]

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

[Kevin Buzzard]

who knows what the element is

[Gabriel Ebner]

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]

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]

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]

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