[Merged by Bors] - chore(Algebra/GroupWithZero/Opposite): Move instances from Algebra.Ring.Opposite

Mathlib.lean

@@ -299,6 +299,7 @@ import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.GroupWithZero.Invertible
 import Mathlib.Algebra.GroupWithZero.NeZero
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
+import Mathlib.Algebra.GroupWithZero.Opposite
 import Mathlib.Algebra.GroupWithZero.Pi
 import Mathlib.Algebra.GroupWithZero.Prod
 import Mathlib.Algebra.GroupWithZero.Semiconj

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau, Devon Tuma, Oliver Nash
 import Mathlib.Algebra.Associated.Basic
 import Mathlib.Algebra.Group.Action.Opposite
 import Mathlib.Algebra.Group.Submonoid.Membership
-import Mathlib.Algebra.Ring.Opposite
+import Mathlib.Algebra.GroupWithZero.Opposite
 
 #align_import ring_theory.non_zero_divisors from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 

Mathlib/Algebra/GroupWithZero/Opposite.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+import Mathlib.Algebra.Group.Opposite
+import Mathlib.Algebra.GroupWithZero.Defs
+
+#align_import algebra.ring.opposite from "leanprover-community/mathlib"@"76de8ae01554c3b37d66544866659ff174e66e1f"
+
+/-!
+# Opposites of groups with zero
+-/
+
+assert_not_exists Ring
+
+variable {α : Type*}
+
+namespace MulOpposite
+
+instance instMulZeroClass [MulZeroClass α] : MulZeroClass αᵐᵒᵖ where
+  zero_mul _ := unop_injective <| mul_zero _
+  mul_zero _ := unop_injective <| zero_mul _
+
+instance instMulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass αᵐᵒᵖ where
+  __ := instMulOneClass
+  __ := instMulZeroClass
+
+instance instSemigroupWithZero [SemigroupWithZero α] : SemigroupWithZero αᵐᵒᵖ where
+  __ := instSemigroup
+  __ := instMulZeroClass
+
+instance instMonoidWithZero [MonoidWithZero α] : MonoidWithZero αᵐᵒᵖ where
+  __ := instMonoid
+  __ := instMulZeroOneClass
+
+instance instNoZeroDivisors [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ where
+  eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
+      Or.casesOn (eq_zero_or_eq_zero_of_mul_eq_zero <| op_injective H)
+        (fun hy => Or.inr <| unop_injective <| hy) fun hx => Or.inl <| unop_injective <| hx
+
+end MulOpposite
+
+namespace AddOpposite
+
+instance instMulZeroClass [MulZeroClass α] : MulZeroClass αᵃᵒᵖ where
+  zero_mul _ := unop_injective <| zero_mul _
+  mul_zero _ := unop_injective <| mul_zero _
+
+instance instMulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass αᵃᵒᵖ where
+  __ := instMulOneClass
+  __ := instMulZeroClass
+
+instance instSemigroupWithZero [SemigroupWithZero α] : SemigroupWithZero αᵃᵒᵖ where
+  __ := instSemigroup
+  __ := instMulZeroClass
+
+instance instMonoidWithZero [MonoidWithZero α] : MonoidWithZero αᵃᵒᵖ where
+  __ := instMonoid
+  __ := instMulZeroOneClass
+
+instance instNoZeroDivisors [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ where
+  eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
+    Or.imp (fun hx => unop_injective hx) (fun hy => unop_injective hy)
+    (@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _ <| op_injective H)
+
+instance instGroupWithZero [GroupWithZero α] : GroupWithZero αᵃᵒᵖ where
+  __ := instMonoidWithZero
+  __ := instNontrivial
+  __ := instDivInvMonoid
+  mul_inv_cancel _ hx := unop_injective <| mul_inv_cancel <| unop_injective.ne hx
+  inv_zero := unop_injective inv_zero
+
+end AddOpposite

Mathlib/Algebra/Module/Defs.lean

@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Hom.End
 import Mathlib.Algebra.Ring.Invertible
+import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Data.Int.Cast.Lemmas
 import Mathlib.GroupTheory.GroupAction.Units

Mathlib/Algebra/Ring/Opposite.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Algebra.Group.Opposite
+import Mathlib.Algebra.GroupWithZero.Opposite
 import Mathlib.Algebra.Ring.Hom.Defs
 
 #align_import algebra.ring.opposite from "leanprover-community/mathlib"@"76de8ae01554c3b37d66544866659ff174e66e1f"
@@ -20,22 +20,6 @@ instance instDistrib [Distrib α] : Distrib αᵐᵒᵖ where
   left_distrib _ _ _ := unop_injective <| add_mul _ _ _
   right_distrib _ _ _ := unop_injective <| mul_add _ _ _
 
-instance instMulZeroClass [MulZeroClass α] : MulZeroClass αᵐᵒᵖ where
-  zero_mul _ := unop_injective <| mul_zero _
-  mul_zero _ := unop_injective <| zero_mul _
-
-instance instMulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass αᵐᵒᵖ where
-  __ := instMulOneClass
-  __ := instMulZeroClass
-
-instance instSemigroupWithZero [SemigroupWithZero α] : SemigroupWithZero αᵐᵒᵖ where
-  __ := instSemigroup
-  __ := instMulZeroClass
-
-instance instMonoidWithZero [MonoidWithZero α] : MonoidWithZero αᵐᵒᵖ where
-  __ := instMonoid
-  __ := instMulZeroOneClass
-
 instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring α] :
     NonUnitalNonAssocSemiring αᵐᵒᵖ where
   __ := instAddCommMonoid
@@ -89,11 +73,6 @@ instance instCommRing [CommRing α] : CommRing αᵐᵒᵖ where
   __ := instRing
   __ := instCommMonoid
 
-instance instNoZeroDivisors [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ where
-  eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
-      Or.casesOn (eq_zero_or_eq_zero_of_mul_eq_zero <| op_injective H)
-        (fun hy => Or.inr <| unop_injective <| hy) fun hx => Or.inl <| unop_injective <| hx
-
 instance instIsDomain [Ring α] [IsDomain α] : IsDomain αᵐᵒᵖ :=
   NoZeroDivisors.to_isDomain _
 
@@ -112,22 +91,6 @@ instance instDistrib [Distrib α] : Distrib αᵃᵒᵖ where
   left_distrib _ _ _ := unop_injective <| mul_add _ _ _
   right_distrib _ _ _ := unop_injective <| add_mul _ _ _
 
-instance instMulZeroClass [MulZeroClass α] : MulZeroClass αᵃᵒᵖ where
-  zero_mul _ := unop_injective <| zero_mul _
-  mul_zero _ := unop_injective <| mul_zero _
-
-instance instMulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass αᵃᵒᵖ where
-  __ := instMulOneClass
-  __ := instMulZeroClass
-
-instance instSemigroupWithZero [SemigroupWithZero α] : SemigroupWithZero αᵃᵒᵖ where
-  __ := instSemigroup
-  __ := instMulZeroClass
-
-instance instMonoidWithZero [MonoidWithZero α] : MonoidWithZero αᵃᵒᵖ where
-  __ := instMonoid
-  __ := instMulZeroOneClass
-
 instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring α] :
     NonUnitalNonAssocSemiring αᵃᵒᵖ where
   __ := instAddCommMonoid
@@ -181,21 +144,9 @@ instance instCommRing [CommRing α] : CommRing αᵃᵒᵖ where
   __ := instRing
   __ := instCommMonoid
 
-instance instNoZeroDivisors [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ where
-  eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
-    Or.imp (fun hx => unop_injective hx) (fun hy => unop_injective hy)
-    (@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _ <| op_injective H)
-
 instance instIsDomain [Ring α] [IsDomain α] : IsDomain αᵃᵒᵖ :=
   NoZeroDivisors.to_isDomain _
 
-instance instGroupWithZero [GroupWithZero α] : GroupWithZero αᵃᵒᵖ where
-  __ := instMonoidWithZero
-  __ := instNontrivial
-  __ := instDivInvMonoid
-  mul_inv_cancel _ hx := unop_injective <| mul_inv_cancel <| unop_injective.ne hx
-  inv_zero := unop_injective inv_zero
-
 end AddOpposite
 
 open MulOpposite

Mathlib/Algebra/SMulWithZero.lean

@@ -6,8 +6,9 @@ Authors: Damiano Testa
 import Mathlib.Algebra.Group.Action.Opposite
 import Mathlib.Algebra.Group.Action.Prod
 import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.GroupWithZero.Opposite
 import Mathlib.Algebra.GroupWithZero.Prod
-import Mathlib.Algebra.Ring.Opposite
+import Mathlib.Algebra.Ring.Defs
 
 #align_import algebra.smul_with_zero from "leanprover-community/mathlib"@"966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2"