From d412cfd086abadf27b7d03f1e534e55f6cd4d162 Mon Sep 17 00:00:00 2001
From: Amelia Livingston <al3717@ic.ac.uk>
Date: Thu, 14 May 2020 15:22:51 +0000
Subject: [PATCH] chore(algebra/ring): lemmas about units in a semiring (#2680)

The lemmas in non-localization files from #2675. (Apart from one, which wasn't relevant to #2675).

(Edit: I am bad at git. I was hoping there would only be 1 commit here. I hope whatever I'm doing wrong is inconsequential...)
---
 src/algebra/group/is_unit.lean |  8 ++++++++
 src/algebra/ring.lean          | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+)

diff --git a/src/algebra/group/is_unit.lean b/src/algebra/group/is_unit.lean
index df81cecb5dc7b..b6158d63c1f24 100644
--- a/src/algebra/group/is_unit.lean
+++ b/src/algebra/group/is_unit.lean
@@ -92,3 +92,11 @@ units.mul_lift_right_inv (λ y, (classical.some_spec $ h y).symm) x
 @[simp, to_additive] lemma is_unit.lift_right_inv_mul [monoid M] [monoid N] (f : M →* N)
   (h : ∀ x, is_unit (f x)) (x) : ↑(is_unit.lift_right f h x)⁻¹ * f x = 1 :=
 units.lift_right_inv_mul (λ y, (classical.some_spec $ h y).symm) x
+
+@[to_additive] theorem is_unit.mul_right_inj [monoid M] {a b c : M} (ha : is_unit a) :
+  a * b = a * c ↔ b = c :=
+by cases ha with a ha; rw [ha, units.mul_right_inj]
+
+@[to_additive] theorem is_unit.mul_left_inj [monoid M] {a b c : M} (ha : is_unit a) :
+  b * a = c * a ↔ b = c :=
+by cases ha with a ha; rw [ha, units.mul_left_inj]
\ No newline at end of file
diff --git a/src/algebra/ring.lean b/src/algebra/ring.lean
index d0dbbfa0f6f46..c8d8814075bcb 100644
--- a/src/algebra/ring.lean
+++ b/src/algebra/ring.lean
@@ -669,6 +669,21 @@ end
 
 namespace units
 
+section semiring
+variables [semiring α]
+
+@[simp] theorem mul_left_eq_zero_iff_eq_zero
+  {r : α} (u : units α) : r * u = 0 ↔ r = 0 :=
+⟨λ h, (mul_left_inj u).1 $ (zero_mul (u : α)).symm ▸ h,
+ λ h, h.symm ▸ zero_mul (u : α)⟩
+
+@[simp] theorem mul_right_eq_zero_iff_eq_zero
+  {r : α} (u : units α) : (u : α) * r = 0 ↔ r = 0 :=
+⟨λ h, (mul_right_inj u).1 $ (mul_zero (u : α)).symm ▸ h,
+ λ h, h.symm ▸ mul_zero (u : α)⟩
+
+end semiring
+
 section comm_semiring
 variables [comm_semiring α] (a b : α) (u : units α)
 
@@ -707,6 +722,23 @@ end domain
 
 end units
 
+namespace is_unit
+
+section semiring
+variables [semiring α]
+
+theorem mul_left_eq_zero_iff_eq_zero {r u : α}
+  (hu : is_unit u) : r * u = 0 ↔ r = 0 :=
+by cases hu with u hu; exact hu.symm ▸ units.mul_left_eq_zero_iff_eq_zero u
+
+theorem mul_right_eq_zero_iff_eq_zero {r u : α}
+  (hu : is_unit u) : u * r = 0 ↔ r = 0 :=
+by cases hu with u hu; exact hu.symm ▸ units.mul_right_eq_zero_iff_eq_zero u
+
+end semiring
+
+end is_unit
+
 /-- A predicate to express that a ring is an integral domain.
 
 This is mainly useful because such a predicate does not contain data,