Typeclass for nontrivial (semi)rings

Stream: Is there code for X?

[Jun Yoshida]

I want to assume a (semi)ring R to be nontrivial or, more explicitly (1 : R) ≠ 0. What is the standard typeclass for this assumption?
I found

• Nontrivial R, but I couldn't find a lemma which explicitly states 1 ≠ 0 in spite of its docstring;
• NeZero 1, but the instance of this class is fewer than the above. I am not sure if this is ok in the undergrad math.

If you have any experience with these classes, I am glad if you could share it.

[Riccardo Brasca]

It is surely Nontrivial R. What exact? says if you ask to prove 0 ≠ 1? (Note that I reversed the order of 0and 1).

[Riccardo Brasca]

This

example (R : Type) [Ring R] [Nontrivial R] : (0 : R) ≠ 1 := zero_ne_one

works. So there some instance that tells Lean that Nontrivial R implies NeZero 1.

[Riccardo Brasca]

Of course for rings they're equivalent, but I would say that Nontrivial is the standard choice in the algebra section of Mathlib.

[Ruben Van de Velde]

docs#NeZero.one

[Jun Yoshida]

Oh, thanks. That's what I want.
(I was a bit surprised seeing the contents of Mathlib.Algebra.GroupWithZero.NeZero lying directly in the global namespace)