trivial module, etc

Stream: Is there code for X?

[Winston Yin]

What's the easiest way to say "let V be a non-zero (non-trivial) vector space" or "show that H is a non-trivial group", etc?

[Riccardo Brasca]

There is docs#nontrivial

[Riccardo Brasca]

Note that it is a class, so you should use it as lemma foo {M : Type*} ... [nontrivial M] : ...

[Winston Yin]

Thanks!