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

@@ -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]

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,