Mul eq implies a ne 0 (for div_ring)

Stream: Is there code for X?

[Ben]

Looking for a lemma like... is it even true :joy:?

example {R: Type} [division_ring R] (a b: R) : a * b = 1 → a ≠ 0 := begin
  assume h1,
  sorry
end

[Riccardo Brasca]

In general it is (much) better to have a math proof before starting formalizing stuff. So first of all you should find a pen and paper proof, and then think about the formalization (for example, do you know that a ≠ 0 means a = 0 → false in Lean?).

[Ben]

Ya I sort of understand all the parts. Hoping writing it out in Lean makes me see how it all goes together. I now have the following

example {R: Type} [division_ring R] (a b: R) : a * b = 1 → a ≠ 0 := begin
  assume h1,
  rw ne.def,
  assume eq_zero,
  rw [eq_zero, zero_mul] at h1,
  have h2 := zero_ne_one,
  contradiction
end

But it fails here because zero_ne_one is based on mul_zero_one_class (or something like that) and doesn't like it that I am using it in the context of a ring.