Zulip Chat Archive

Stream: Is there code for X?

Topic: Cancelling in a domain


view this post on Zulip Adam Topaz (Mar 18 2021 at 21:55):

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

view this post on Zulip 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)

view this post on Zulip 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