chore(Algebra/Group): Do not import GroupWithZero (#11202)

I am claiming that anything within the `Algebra.Group` folder should be additivisable, to the exception of `MonoidHom.End` maybe. This is not the case of `NeZero`, `MonoidWithZero` and `MonoidWithZeroHom` which were all imported to prove a few lemmas. Those lemmas are easily moved to another file.

Mathlib/Algebra/Group/Equiv/Basic.lean

@@ -149,22 +149,6 @@ instance (priority := 100) instMonoidHomClass
 
 variable [EquivLike F α β]
 
--- See note [lower instance priority]
-instance (priority := 100) toZeroHomClass
-    [MulZeroClass α] [MulZeroClass β] [MulEquivClass F α β] :
-    ZeroHomClass F α β where
-  map_zero := fun e =>
-    calc
-      e 0 = e 0 * e (EquivLike.inv e 0) := by rw [← map_mul, zero_mul]
-        _ = 0 := by simp
-
--- See note [lower instance priority]
-instance (priority := 100) toMonoidWithZeroHomClass
-    [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] :
-    MonoidWithZeroHomClass F α β :=
-  { MulEquivClass.instMonoidHomClass F, MulEquivClass.toZeroHomClass F with }
-#align mul_equiv_class.to_monoid_with_zero_hom_class MulEquivClass.toMonoidWithZeroHomClass
-
 variable {F}
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Group/Hom/Basic.lean

@@ -5,8 +5,7 @@ Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hu
   Johannes Hölzl, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.GroupWithZero.Hom
-import Mathlib.Algebra.NeZero
+import Mathlib.Algebra.Group.Hom.Defs
 
 #align_import algebra.hom.group from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
@@ -15,6 +14,9 @@ import Mathlib.Algebra.NeZero
 
 -/
 
+-- `NeZero` cannot be additivised, hence its theory should be developed outside of the
+-- `Algebra.Group` folder.
+assert_not_exists NeZero
 
 variable {α β M N P : Type*}
 
@@ -24,23 +26,6 @@ variable {G : Type*} {H : Type*}
 -- groups
 variable {F : Type*}
 
-namespace NeZero
-
-theorem of_map {R M} [Zero R] [Zero M] [FunLike F R M] [ZeroHomClass F R M]
-    (f : F) {r : R} [neZero : NeZero (f r)] : NeZero r :=
-  ⟨fun h => ne (f r) <| by rw [h]; exact ZeroHomClass.map_zero f⟩
-#align ne_zero.of_map NeZero.of_map
-
-theorem of_injective {R M} [Zero R] {r : R} [NeZero r] [Zero M] [FunLike F R M]
-    [ZeroHomClass F R M] {f : F}
-    (hf : Function.Injective f) : NeZero (f r) :=
-  ⟨by
-    rw [← ZeroHomClass.map_zero f]
-    exact hf.ne NeZero.out⟩
-#align ne_zero.of_injective NeZero.of_injective
-
-end NeZero
-
 section DivisionCommMonoid
 
 variable [DivisionCommMonoid α]
@@ -261,11 +246,3 @@ lemma comp_div (f : G →* H) (g h : M →* G) : f.comp (g / h) = f.comp g / f.c
   ext; simp only [Function.comp_apply, div_apply, map_div, coe_comp]
 
 end InvDiv
-
-/-- Given two monoid with zero morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid
-with zero morphism sending `x` to `f x * g x`. -/
-instance [MulZeroOneClass M] [CommMonoidWithZero N] : Mul (M →*₀ N) :=
-  ⟨fun f g => { (f * g : M →* N) with
-    toFun := fun a => f a * g a,
-    map_zero' := by dsimp only []; rw [map_zero, zero_mul] }⟩
-    -- Porting note: why do we need `dsimp` here?

Mathlib/Algebra/Group/Prod.lean

@@ -5,6 +5,7 @@ Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.Units.Hom
+import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 
 #align_import algebra.group.prod from "leanprover-community/mathlib"@"cd391184c85986113f8c00844cfe6dda1d34be3d"

Mathlib/Algebra/GroupWithZero/Hom.lean

@@ -3,8 +3,9 @@ Copyright (c) 2020 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.GroupWithZero.Defs
+import Mathlib.Algebra.NeZero
 
 #align_import algebra.hom.group from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
@@ -35,6 +36,19 @@ monoid homomorphism
 
 open Function
 
+namespace NeZero
+variable {F α β  : Type*} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] {a : α}
+
+lemma of_map (f : F) [neZero : NeZero (f a)] : NeZero a :=
+  ⟨fun h ↦ ne (f a) <| by rw [h]; exact ZeroHomClass.map_zero f⟩
+#align ne_zero.of_map NeZero.of_map
+
+lemma of_injective {f : F} (hf : Injective f) [NeZero a] : NeZero (f a) :=
+  ⟨by rw [← ZeroHomClass.map_zero f]; exact hf.ne NeZero.out⟩
+#align ne_zero.of_injective NeZero.of_injective
+
+end NeZero
+
 variable {F α β γ δ : Type*} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ]
   [MulZeroOneClass δ]
 
@@ -234,3 +248,34 @@ lemma toZeroHom_injective : Injective (toZeroHom : (α →*₀ β) → ZeroHom 
 
 -- Unlike the other homs, `MonoidWithZeroHom` does not have a `1` or `0`
 instance : Inhabited (α →*₀ α) := ⟨id α⟩
+
+/-- Given two monoid with zero morphisms `f`, `g` to a commutative monoid with zero, `f * g` is the
+monoid with zero morphism sending `x` to `f x * g x`. -/
+instance {β} [CommMonoidWithZero β] : Mul (α →*₀ β) where
+  mul f g :=
+    { (f * g : α →* β) with
+      map_zero' := by dsimp; rw [map_zero, zero_mul] }
+
+end MonoidWithZeroHom
+
+/-! ### Equivalences -/
+
+namespace MulEquivClass
+variable {F α β : Type*} [EquivLike F α β]
+
+-- See note [lower instance priority]
+instance (priority := 100) toZeroHomClass [MulZeroClass α] [MulZeroClass β] [MulEquivClass F α β] :
+    ZeroHomClass F α β where
+  map_zero f :=
+    calc
+      f 0 = f 0 * f (EquivLike.inv f 0) := by rw [← map_mul, zero_mul]
+        _ = 0 := by simp
+
+-- See note [lower instance priority]
+instance (priority := 100) toMonoidWithZeroHomClass
+    [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] :
+    MonoidWithZeroHomClass F α β :=
+  { MulEquivClass.instMonoidHomClass F, MulEquivClass.toZeroHomClass with }
+#align mul_equiv_class.to_monoid_with_zero_hom_class MulEquivClass.toMonoidWithZeroHomClass
+
+end MulEquivClass

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.Commute.Units
-import Mathlib.Algebra.Group.Hom.Basic
 import Mathlib.Algebra.Group.Units.Hom
 import Mathlib.Algebra.GroupWithZero.Commute
+import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.GroupTheory.GroupAction.Units
 

Mathlib/Algebra/Order/Hom/Monoid.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.Group.Hom.Basic
+import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.Order.Group.Instances
 import Mathlib.Algebra.Order.Monoid.WithZero.Defs
 import Mathlib.Order.Hom.Basic