NeZero on Rings

Stream: mathlib4

[Steven Rossi]

Is there a NeZero condition on the one of rings? Just noticing that simp isn’t getting \not 0=1

[Ruben Van de Velde]

Does apply zero_ne_one work?

[Antoine Chambert-Loir]

To provide context, docs#zero_ne_one requires Zero R, One R, and NeZero 1, and the latter is provided by docs#ZeroNe.one which holds if R is a nontrivial MonoidWithZero.

[Eric Wieser]

Perhaps worth remembering that Ring Unit exists, and there 0 = 1!

[Antoine Chambert-Loir]

Of course. (Sweats) But yes, I had mentioned nontrivial.

[Eric Wieser]

Sorry, my remark was directed at Steven, your comment was indeed correct :)