feat: port Algebra.Hom.Equiv.Units.GroupWithZero (#901)

mathlib3 655994e298904d7e5bbd1e18c95defd7b543eb94

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Author: hrmacbeth

Mathlib.lean

@@ -30,6 +30,7 @@ import Mathlib.Algebra.Hom.Commute
 import Mathlib.Algebra.Hom.Embedding
 import Mathlib.Algebra.Hom.Equiv.Basic
 import Mathlib.Algebra.Hom.Equiv.Units.Basic
+import Mathlib.Algebra.Hom.Equiv.Units.GroupWithZero
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Algebra.Hom.Units
 import Mathlib.Algebra.Homology.ComplexShape

Mathlib/Algebra/Hom/Equiv/Units/GroupWithZero.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
+-/
+import Mathlib.Algebra.Hom.Equiv.Units.Basic
+import Mathlib.Algebra.GroupWithZero.Units.Basic
+
+/-!
+# Multiplication by a nonzero element in a `GroupWithZero` is a permutation.
+-/
+
+
+variable {G : Type _}
+
+namespace Equiv
+
+section GroupWithZero
+
+variable [GroupWithZero G]
+
+/-- Left multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
+underlying type. -/
+@[simps (config := { fullyApplied := false })]
+protected def mulLeft₀ (a : G) (ha : a ≠ 0) : Perm G :=
+  (Units.mk0 a ha).mulLeft
+#align equiv.mul_left₀ Equiv.mulLeft₀
+
+theorem mulLeft_bijective₀ (a : G) (ha : a ≠ 0) : Function.Bijective ((· * ·) a : G → G) :=
+  (Equiv.mulLeft₀ a ha).bijective
+#align equiv.mul_left_bijective₀ Equiv.mulLeft_bijective₀
+
+/-- Right multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
+underlying type. -/
+@[simps (config := { fullyApplied := false })]
+protected def mulRight₀ (a : G) (ha : a ≠ 0) : Perm G :=
+  (Units.mk0 a ha).mulRight
+#align equiv.mul_right₀ Equiv.mulRight₀
+
+theorem mulRight_bijective₀ (a : G) (ha : a ≠ 0) : Function.Bijective ((· * a) : G → G) :=
+  (Equiv.mulRight₀ a ha).bijective
+#align equiv.mul_right_bijective₀ Equiv.mulRight_bijective₀
+
+end GroupWithZero
+
+end Equiv