feat(algebra/regular): add lemmas about regularity of non-zero elemen…

…ts (#6579)

More API, to deal with cases in which a regular element is non-zero.

src/algebra/regular.lean

@@ -49,12 +49,12 @@ section semigroup
 
 variable [semigroup R]
 
-/-- In a semigroup, then the product of left-regular elements is left-regular. -/
+/-- In a semigroup, the product of left-regular elements is left-regular. -/
 lemma is_left_regular.mul (lra : is_left_regular a) (lrb : is_left_regular b) :
   is_left_regular (a * b) :=
 show function.injective ((*) (a * b)), from (comp_mul_left a b) ▸ lra.comp lrb
 
-/-- In a semigroup, then the product of right-regular elements is right-regular. -/
+/-- In a semigroup, the product of right-regular elements is right-regular. -/
 lemma is_right_regular.mul (rra : is_right_regular a) (rrb : is_right_regular b) :
   is_right_regular (a * b) :=
 show function.injective (* (a * b)), from (comp_mul_right b a) ▸ rrb.comp rra
@@ -205,6 +205,28 @@ lemma is_regular_iff_subsingleton : is_regular (0 : R) ↔ subsingleton R :=
 ⟨λ h, h.left.subsingleton,
  λ h, ⟨is_left_regular_zero_iff_subsingleton.mpr h, is_right_regular_zero_iff_subsingleton.mpr h⟩⟩
 
+/-- A left-regular element of a `nontrivial` `mul_zero_class` is non-zero. -/
+lemma is_left_regular.ne_zero [nontrivial R] (la : is_left_regular a) : a ≠ 0 :=
+begin
+  rintro rfl,
+  rcases exists_pair_ne R with ⟨x, y, xy⟩,
+  refine xy (la _),
+  rw [zero_mul, zero_mul]
+end
+
+/-- A right-regular element of a `nontrivial` `mul_zero_class` is non-zero. -/
+lemma is_right_regular.ne_zero [nontrivial R] (ra : is_right_regular a) : a ≠ 0 :=
+begin
+  rintro rfl,
+  rcases exists_pair_ne R with ⟨x, y, xy⟩,
+  refine xy (ra (_ : x * 0 = y * 0)),
+  rw [mul_zero, mul_zero]
+end
+
+/-- A regular element of a `nontrivial` `mul_zero_class` is non-zero. -/
+lemma is_regular.ne_zero [nontrivial R] (la : is_regular a) : a ≠ 0 :=
+la.left.ne_zero
+
 end mul_zero_class
 
 section comm_semigroup
@@ -282,4 +304,8 @@ variables  [cancel_monoid_with_zero R]
 lemma is_regular_of_ne_zero (a0 : a ≠ 0) : is_regular a :=
 ⟨λ b c, (mul_right_inj' a0).mp, λ b c, (mul_left_inj' a0).mp⟩
 
+/-- In a non-trivial integral domain, an element is regular iff it is non-zero. -/
+lemma is_regular_iff_ne_zero [nontrivial R] : is_regular a ↔ a ≠ 0 :=
+⟨is_regular.ne_zero, is_regular_of_ne_zero⟩
+
 end cancel_monoid_with_zero