refactor(algebra/*): streamlining up to data.nat.cast.basic (#17530)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/euclidean_domain/instances.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
 -/
 import algebra.euclidean_domain.defs
-import algebra.group_with_zero.units
+import algebra.group_with_zero.units.lemmas
 import data.nat.order.basic
 import data.int.order.basic
 

src/algebra/field/basic.lean

@@ -6,6 +6,7 @@ Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 import data.rat.defs
 import algebra.field.defs
 import algebra.ring.basic
+import algebra.group_with_zero.units.lemmas
 
 /-!
 # Lemmas about division (semi)rings and (semi)fields

src/algebra/group/with_one.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro, Johan Commelin
 -/
 import order.bounded_order
 import algebra.hom.equiv.basic
-import algebra.group_with_zero.units
+import algebra.group_with_zero.units.basic
 import algebra.ring.defs
 
 /-!

src/algebra/group_power/ring.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import algebra.group_power.basic
-import algebra.group_with_zero.units
+import algebra.group_with_zero.commute
 import algebra.hom.ring
 import algebra.ring.commute
 import data.nat.order.lemmas

src/algebra/group_with_zero/commute.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+import algebra.group_with_zero.semiconj
+import algebra.group.commute
+import tactic.nontriviality
+
+/-!
+# Lemmas about commuting elements in a `monoid_with_zero` or a `group_with_zero`.
+
+-/
+
+variables {α M₀ G₀ M₀' G₀' F F' : Type*}
+
+variables [monoid_with_zero M₀]
+
+namespace ring
+open_locale classical
+
+lemma mul_inverse_rev' {a b : M₀} (h : commute a b) : inverse (a * b) = inverse b * inverse a :=
+begin
+  by_cases hab : is_unit (a * b),
+  { obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.is_unit_mul_iff.mp hab,
+    rw [←units.coe_mul, inverse_unit, inverse_unit, inverse_unit, ←units.coe_mul,
+      mul_inv_rev], },
+  obtain ha | hb := not_and_distrib.mp (mt h.is_unit_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]},
+end
+
+lemma mul_inverse_rev {M₀} [comm_monoid_with_zero M₀] (a b : M₀) :
+  ring.inverse (a * b) = inverse b * inverse a :=
+mul_inverse_rev' (commute.all _ _)
+
+end ring
+
+lemma 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
+
+namespace commute
+
+@[simp] theorem zero_right [mul_zero_class G₀] (a : G₀) : commute a 0 := semiconj_by.zero_right a
+@[simp] theorem zero_left [mul_zero_class G₀] (a : G₀) : commute 0 a := semiconj_by.zero_left a a
+
+variables [group_with_zero G₀] {a b c : G₀}
+
+@[simp] theorem inv_left_iff₀ : commute a⁻¹ b ↔ commute a b :=
+semiconj_by.inv_symm_left_iff₀
+
+theorem inv_left₀ (h : commute a b) : commute a⁻¹ b := inv_left_iff₀.2 h
+
+@[simp] theorem inv_right_iff₀ : commute a b⁻¹ ↔ commute a b :=
+semiconj_by.inv_right_iff₀
+
+theorem inv_right₀ (h : commute a b) : commute a b⁻¹ := inv_right_iff₀.2 h
+
+@[simp] theorem div_right (hab : commute a b) (hac : commute a c) :
+  commute a (b / c) :=
+hab.div_right hac
+
+@[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₀ }
+
+end commute

src/algebra/group_with_zero/semiconj.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+import algebra.group_with_zero.units.basic
+import algebra.group.semiconj
+
+/-!
+# Lemmas about semiconjugate elements in a `group_with_zero`.
+
+-/
+
+variables {α M₀ G₀ M₀' G₀' F F' : Type*}
+
+namespace semiconj_by
+
+@[simp] lemma zero_right [mul_zero_class G₀] (a : G₀) : semiconj_by a 0 0 :=
+by simp only [semiconj_by, mul_zero, zero_mul]
+
+@[simp] lemma zero_left [mul_zero_class G₀] (x y : G₀) : semiconj_by 0 x y :=
+by simp only [semiconj_by, mul_zero, zero_mul]
+
+variables [group_with_zero G₀] {a x y x' y' : G₀}
+
+@[simp] lemma inv_symm_left_iff₀ : semiconj_by a⁻¹ x y ↔ semiconj_by a y x :=
+classical.by_cases
+  (λ ha : a = 0, by simp only [ha, inv_zero, semiconj_by.zero_left])
+  (λ ha, @units_inv_symm_left_iff _ _ (units.mk0 a ha) _ _)
+
+lemma inv_symm_left₀ (h : semiconj_by a x y) : semiconj_by a⁻¹ y x :=
+semiconj_by.inv_symm_left_iff₀.2 h
+
+lemma inv_right₀ (h : semiconj_by a x y) : semiconj_by a x⁻¹ y⁻¹ :=
+begin
+  by_cases ha : a = 0,
+  { simp only [ha, zero_left] },
+  by_cases hx : x = 0,
+  { subst x,
+    simp only [semiconj_by, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h,
+    simp [h.resolve_right ha] },
+  { have := mul_ne_zero ha hx,
+    rw [h.eq, mul_ne_zero_iff] at this,
+    exact @units_inv_right _ _ _ (units.mk0 x hx) (units.mk0 y this.1) h },
+end
+
+@[simp] lemma inv_right_iff₀ : semiconj_by a x⁻¹ y⁻¹ ↔ semiconj_by a x y :=
+⟨λ h, inv_inv x ▸ inv_inv y ▸ h.inv_right₀, inv_right₀⟩
+
+lemma div_right (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
+  semiconj_by a (x / x') (y / y') :=
+by { rw [div_eq_mul_inv, div_eq_mul_inv], exact h.mul_right h'.inv_right₀ }
+
+end semiconj_by