feat(Algebra/GroupWithZero/Commute): port file (#762)

mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636

porting notes: easy

1. There were two lemmas that had been ad hoc ported into Algebra.Ring.Basic, which caused these to be marked as dubious translations by Mathport (because the type class assumptions didn't match), so I have just `#align`ed them *without* an `ₓ` here.

Co-authored-by: Scott Morrison <[email protected]>

Mathlib.lean

@@ -13,6 +13,7 @@ import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupPower.Identities
 import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.GroupWithZero.Semiconj

Mathlib/Algebra/GroupWithZero/Commute.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+import Mathlib.Algebra.GroupWithZero.Semiconj
+import Mathlib.Algebra.Group.Commute
+import Mathlib.Tactic.Nontriviality
+
+/-!
+# Lemmas about commuting elements in a `MonoidWithZero` or a `GroupWithZero`.
+
+-/
+
+
+variable {α M₀ G₀ M₀' G₀' F F' : Type _}
+
+variable [MonoidWithZero M₀]
+
+namespace Ring
+
+open Classical
+
+theorem mul_inverse_rev' {a b : M₀} (h : Commute a b) :
+    inverse (a * b) = inverse b * inverse a := by
+  by_cases hab : IsUnit (a * b)
+  · obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
+    rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
+  obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
+  · rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
+  · rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]
+#align ring.mul_inverse_rev' Ring.mul_inverse_rev'
+
+theorem mul_inverse_rev {M₀} [CommMonoidWithZero M₀] (a b : M₀) :
+    Ring.inverse (a * b) = inverse b * inverse a :=
+  mul_inverse_rev' (Commute.all _ _)
+#align ring.mul_inverse_rev Ring.mul_inverse_rev
+
+end Ring
+
+theorem Commute.ring_inverse_ring_inverse {a b : M₀} (h : Commute a b) :
+    Commute (Ring.inverse a) (Ring.inverse b) :=
+  (Ring.mul_inverse_rev' h.symm).symm.trans <| (congr_arg _ h.symm.eq).trans <|
+    Ring.mul_inverse_rev' h
+#align commute.ring_inverse_ring_inverse Commute.ring_inverse_ring_inverse
+
+namespace Commute
+
+@[simp]
+theorem zero_right [MulZeroClass G₀] (a : G₀) : Commute a 0 :=
+  SemiconjBy.zero_right a
+#align commute.zero_right Commute.zero_right
+
+@[simp]
+theorem zero_left [MulZeroClass G₀] (a : G₀) : Commute 0 a :=
+  SemiconjBy.zero_left a a
+#align commute.zero_left Commute.zero_left
+
+variable [GroupWithZero G₀] {a b c : G₀}
+
+@[simp]
+theorem inv_left_iff₀ : Commute a⁻¹ b ↔ Commute a b :=
+  SemiconjBy.inv_symm_left_iff₀
+#align commute.inv_left_iff₀ Commute.inv_left_iff₀
+
+theorem inv_left₀ (h : Commute a b) : Commute a⁻¹ b :=
+  inv_left_iff₀.2 h
+#align commute.inv_left₀ Commute.inv_left₀
+
+@[simp]
+theorem inv_right_iff₀ : Commute a b⁻¹ ↔ Commute a b :=
+  SemiconjBy.inv_right_iff₀
+#align commute.inv_right_iff₀ Commute.inv_right_iff₀
+
+theorem inv_right₀ (h : Commute a b) : Commute a b⁻¹ :=
+  inv_right_iff₀.2 h
+#align commute.inv_right₀ Commute.inv_right₀
+
+@[simp]
+theorem div_right (hab : Commute a b) (hac : Commute a c) : Commute a (b / c) :=
+  SemiconjBy.div_right hab hac
+#align commute.div_right Commute.div_right
+
+@[simp]
+theorem div_left (hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c := by
+  rw [div_eq_mul_inv]
+  exact hac.mul_left hbc.inv_left₀
+#align commute.div_left Commute.div_left
+
+end Commute

Mathlib/Algebra/Ring/Basic.lean

@@ -1,3 +1,4 @@
+import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.Ring.Commute
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Data.Int.Cast.Basic
@@ -13,13 +14,6 @@ export Distrib (left_distrib right_distrib)
 
 section Semiring
 
--- TODO: put these in the right place
-@[simp] theorem Commute.zero_right [Semiring R] (a : R) : Commute a 0 :=
-  (mul_zero _).trans (zero_mul _).symm
-
-@[simp] theorem Commute.zero_left [Semiring R] (a : R) : Commute 0 a :=
-  (zero_mul _).trans (mul_zero _).symm
-
 @[simp]
 lemma Nat.cast_mul [Semiring R] {m n : ℕ} : (m * n).cast = (m.cast * n.cast : R) := by
   induction n generalizing m <;> simp_all [mul_succ, mul_add]