feat(data/equiv/mul_add): add lemmas about multiplication and additio…

…n on a group being bijective and finite cancel_monoid_with_zeros (#10046)

src/data/equiv/mul_add.lean

@@ -440,6 +440,10 @@ def mul_left (u : units M) : equiv.perm M :=
 lemma mul_left_symm (u : units M) : u.mul_left.symm = u⁻¹.mul_left :=
 equiv.ext $ λ x, rfl
 
+@[to_additive]
+lemma mul_left_bijective (a : units M) : function.bijective ((*) a : M → M) :=
+(mul_left a).bijective
+
 /-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/
 @[to_additive "Right addition of an additive unit is a permutation of the underlying type.",
   simps apply {fully_applied := ff}]
@@ -453,6 +457,10 @@ def mul_right (u : units M) : equiv.perm M :=
 lemma mul_right_symm (u : units M) : u.mul_right.symm = u⁻¹.mul_right :=
 equiv.ext $ λ x, rfl
 
+@[to_additive]
+lemma mul_right_bijective (a : units M) : function.bijective ((* a) : M → M) :=
+(mul_right a).bijective
+
 end units
 
 namespace equiv
@@ -475,6 +483,10 @@ lemma mul_left_symm_apply (a : G) : ((equiv.mul_left a).symm : G → G) = (*) a
 lemma mul_left_symm (a : G) : (equiv.mul_left a).symm = equiv.mul_left a⁻¹ :=
 ext $ λ x, rfl
 
+@[to_additive]
+lemma _root_.group.mul_left_bijective (a : G) : function.bijective ((*) a) :=
+(equiv.mul_left a).bijective
+
 /-- Right multiplication in a `group` is a permutation of the underlying type. -/
 @[to_additive "Right addition in an `add_group` is a permutation of the underlying type."]
 protected def mul_right (a : G) : perm G := (to_units a).mul_right
@@ -490,6 +502,10 @@ ext $ λ x, rfl
 @[simp, nolint simp_nf, to_additive]
 lemma mul_right_symm_apply (a : G) : ((equiv.mul_right a).symm : G → G) = λ x, x * a⁻¹ := rfl
 
+@[to_additive]
+lemma _root_.group.mul_right_bijective (a : G) : function.bijective (* a) :=
+(equiv.mul_right a).bijective
+
 variable (G)
 
 /-- Inversion on a `group` is a permutation of the underlying type. -/
@@ -542,12 +558,20 @@ underlying type. -/
 protected def mul_left₀ (a : G) (ha : a ≠ 0) : perm G :=
 (units.mk0 a ha).mul_left
 
+lemma _root_.mul_left_bijective₀ (a : G) (ha : a ≠ 0) :
+  function.bijective ((*) a : G → G) :=
+(equiv.mul_left₀ a ha).bijective
+
 /-- Right multiplication by a nonzero element in a `group_with_zero` is a permutation of the
 underlying type. -/
 @[simps {fully_applied := ff}]
 protected def mul_right₀ (a : G) (ha : a ≠ 0) : perm G :=
 (units.mk0 a ha).mul_right
 
+lemma _root_.mul_right_bijective₀ (a : G) (ha : a ≠ 0) :
+  function.bijective ((* a) : G → G) :=
+(equiv.mul_right₀ a ha).bijective
+
 end group_with_zero
 
 end equiv

src/ring_theory/integral_domain.lean

@@ -30,29 +30,41 @@ section
 open finset polynomial function
 open_locale big_operators nat
 
+section cancel_monoid_with_zero
+-- There doesn't seem to be a better home for these right now
+variables {M : Type*} [cancel_monoid_with_zero M] [fintype M]
+
+lemma mul_right_bijective_of_fintype₀ {a : M} (ha : a ≠ 0) : bijective (λ b, a * b) :=
+fintype.injective_iff_bijective.1 $ mul_right_injective₀ ha
+
+lemma mul_left_bijective_of_fintype₀ {a : M} (ha : a ≠ 0) : bijective (λ b, b * a) :=
+fintype.injective_iff_bijective.1 $ mul_left_injective₀ ha
+
+/-- Every finite nontrivial cancel_monoid_with_zero is a group_with_zero. -/
+def group_with_zero_of_fintype (M : Type*) [cancel_monoid_with_zero M] [decidable_eq M] [fintype M]
+  [nontrivial M] : group_with_zero M :=
+{ inv := λ a, if h : a = 0 then 0 else fintype.bij_inv (mul_right_bijective_of_fintype₀ h) 1,
+  mul_inv_cancel := λ a ha,
+    by { simp [has_inv.inv, dif_neg ha], exact fintype.right_inverse_bij_inv _ _ },
+  inv_zero := by { simp [has_inv.inv, dif_pos rfl] },
+  ..‹nontrivial M›,
+  ..‹cancel_monoid_with_zero M› }
+
+end cancel_monoid_with_zero
+
 variables {R : Type*} {G : Type*}
 
 section ring
 
 variables [ring R] [is_domain R] [fintype R]
 
-lemma mul_right_bijective₀ (a : R) (ha : a ≠ 0) : bijective (λ b, a * b) :=
-fintype.injective_iff_bijective.1 $ mul_right_injective₀ ha
-
-lemma mul_left_bijective₀ (a : R) (ha : a ≠ 0) : bijective (λ b, b * a) :=
-fintype.injective_iff_bijective.1 $ mul_left_injective₀ ha
-
 /-- Every finite domain is a division ring.
 
 TODO: Prove Wedderburn's little theorem,
 which shows a finite domain is in fact commutative, hence a field. -/
 def division_ring_of_is_domain (R : Type*) [ring R] [is_domain R] [decidable_eq R] [fintype R] :
   division_ring R :=
-{ inv := λ a, if h : a = 0 then 0 else fintype.bij_inv (mul_right_bijective₀ a h) 1,
-  mul_inv_cancel := λ a ha, show a * dite _ _ _ = _,
-    by { rw dif_neg ha, exact fintype.right_inverse_bij_inv _ _ },
-  inv_zero := dif_pos rfl,
-  ..show nontrivial R, by apply_instance,
+{ ..show group_with_zero R, from group_with_zero_of_fintype R,
   ..‹ring R› }
 
 end ring