Zulip Chat Archive

Stream: maths

Topic: trivial group / module


view this post on Zulip Kenny Lau (Jul 14 2020 at 06:51):

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

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:53):

unique M?

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:54):

what do we know about it?

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:55):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 03:12):

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


Last updated: May 19 2021 at 00:40 UTC