Zulip Chat Archive

Stream: maths

Topic: trivial group / module

Kenny Lau (Jul 14 2020 at 06:51):

what is the canonical way of saying that a group / module is trivial?

Johan Commelin (Jul 14 2020 at 06:53):

unique M?

Kenny Lau (Jul 14 2020 at 06:54):

what do we know about it?

Johan Commelin (Jul 14 2020 at 06:55):

That it's a type with 1 term... em tasol

Yury G. Kudryashov (Jul 26 2020 at 03:11):

An idea for a simple PR: add all instances of the form instance [subsingleton M] : unique (sub* M) where sub* is one of submonoid, subgroup, submodule.

Yury G. Kudryashov (Jul 26 2020 at 03:12):

(I don't know which of those instances already exist)

Last updated: Dec 20 2023 at 11:08 UTC