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):
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
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