rings are nontrivial iff 0 != 1.

Stream: Is there code for X?

[Kevin Buzzard]

I can't find this:

import Mathlib

lemma NonAssocSemiring.Nontrivial_iff (R : Type) [NonAssocSemiring R] :
  Nontrivial R ↔ (0 : R) ≠ 1 := by
  refine ⟨fun _ ↦ zero_ne_one' R, fun a ↦
    Function.Surjective.groupWithZero.proof_1 a⟩

(and I'm a bit suspicious of the proof exact? gave me...)

[Kevin Buzzard]

Oh this is better:

lemma NonAssocSemiring.Nontrivial_iff (R : Type) [NonAssocSemiring R] :
    Nontrivial R ↔ (0 : R) ≠ 1 :=
  ⟨fun _ ↦ zero_ne_one' R, fun a ↦ ⟨0, 1, a⟩⟩

[Kevin Buzzard]

Function.Surjective.groupWithZero.proof_1.{u_1} {G₀' : Type u_1} [inst✝ : Zero G₀'] [inst✝¹ : One G₀'] (h01 : 0 ≠ 1) :
  Nontrivial G₀'

This could be an aesop safe rule because it's the universal property of Nontrivial.

[Kyle Miller]

Here's it making use of another lemma:

lemma NonAssocSemiring.Nontrivial_iff (R : Type) [NonAssocSemiring R] :
    Nontrivial R ↔ (0 : R) ≠ 1 :=
  ⟨fun _ ↦ zero_ne_one, nontrivial_of_ne _ _⟩

[Kyle Miller]

The difference between zero_ne_one and zero_ne_one' is that the former doesn't take R explicitly.