## Stream: Is there code for X?

### Topic: Cancelling in a domain

#### Adam Topaz (Mar 18 2021 at 21:55):

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 (Mar 19 2021 at 05:13):

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 (Mar 19 2021 at 06:17):

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 _}⟩


Last updated: May 17 2021 at 15:13 UTC