Cancelling in a domain

Stream: Is there code for X?

[Adam Topaz]

What's the name of the lemma which says, in an integral domain, that $a \cdot b = b$ implies $a = 1$? (assuming $b \neq 0$, of course)

[Damiano Testa]

Hmm, I thought that what you wanted was already a lemma, but I could not find it. What is below works, though, also replacing cancel_monoid_with_zero with integral_domain:

import algebra.group_with_zero.basic

lemma mul_left_cancel'' {R : Type*} [cancel_monoid_with_zero R] {a b : R}
  (b0 : b ≠ 0) (ab : a * b = b) :
  a = 1 :=
(mul_left_inj' b0).mp (ab.trans (one_mul _).symm)

[Damiano Testa]

Actually, maybe these versions are more useful:

lemma mul_eq_self_right_iff {R : Type*} [cancel_monoid_with_zero R] {a b : R}
  (b0 : b ≠ 0) :
  a * b = b ↔ a = 1 :=
⟨λ ab, (mul_left_inj' b0).mp (ab.trans (one_mul _).symm), by {rintro rfl, exact one_mul _}⟩

lemma mul_eq_self_left_iff {R : Type*} [cancel_monoid_with_zero R] {a b : R}
  (b0 : a ≠ 0) :
  a * b = a ↔ b = 1 :=
⟨λ ab, (mul_right_inj' b0).mp (ab.trans (mul_one _).symm), by {rintro rfl, exact mul_one _}⟩