chore: split Mathlib.Algebra.Invertible (#6973)

`Mathlib.Algebra.Invertible` is used by fundamental tactics, and this essentially splits it into the part used by `NormNum`, and everything else.



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

Mathlib.lean

@@ -242,7 +242,9 @@ import Mathlib.Algebra.Homology.ShortExact.Abelian
 import Mathlib.Algebra.Homology.ShortExact.Preadditive
 import Mathlib.Algebra.Homology.Single
 import Mathlib.Algebra.IndicatorFunction
-import Mathlib.Algebra.Invertible
+import Mathlib.Algebra.Invertible.Basic
+import Mathlib.Algebra.Invertible.Defs
+import Mathlib.Algebra.Invertible.GroupWithZero
 import Mathlib.Algebra.IsPrimePow
 import Mathlib.Algebra.Jordan.Basic
 import Mathlib.Algebra.Lie.Abelian

Mathlib/Algebra/CharP/Invertible.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import Mathlib.Algebra.Invertible
 import Mathlib.Algebra.CharP.Basic
 
 #align_import algebra.char_p.invertible from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import Mathlib.Algebra.Invertible
+import Mathlib.Algebra.Invertible.Basic
 import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.Order.Monoid.WithTop

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -187,7 +187,6 @@ theorem mul_right_eq_self₀ : a * b = a ↔ b = 1 ∨ a = 0 :=
     _ ↔ b = 1 ∨ a = 0 := mul_eq_mul_left_iff
 #align mul_right_eq_self₀ mul_right_eq_self₀
 
-
 theorem mul_left_eq_self₀ : a * b = b ↔ a = 1 ∨ b = 0 :=
   calc
     a * b = b ↔ a * b = 1 * b := by rw [one_mul]
@@ -230,37 +229,6 @@ section GroupWithZero
 
 variable [GroupWithZero G₀] {a b c g h x : G₀}
 
-@[simp]
-theorem mul_inv_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a :=
-  calc
-    a * b * b⁻¹ = a * (b * b⁻¹) := mul_assoc _ _ _
-    _ = a := by simp [h]
-#align mul_inv_cancel_right₀ mul_inv_cancel_right₀
-
-
-@[simp]
-theorem mul_inv_cancel_left₀ (h : a ≠ 0) (b : G₀) : a * (a⁻¹ * b) = b :=
-  calc
-    a * (a⁻¹ * b) = a * a⁻¹ * b := (mul_assoc _ _ _).symm
-    _ = b := by simp [h]
-#align mul_inv_cancel_left₀ mul_inv_cancel_left₀
-
-
--- Porting note: used `simpa` to prove `False` in lean3
-theorem inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 := fun a_eq_0 => by
-  have := mul_inv_cancel h
-  simp [a_eq_0] at this
-#align inv_ne_zero inv_ne_zero
-
-@[simp]
-theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 :=
-  calc
-    a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ := by simp [inv_ne_zero h]
-    _ = a⁻¹ * a⁻¹⁻¹ := by simp [h]
-    _ = 1 := by simp [inv_ne_zero h]
-#align inv_mul_cancel inv_mul_cancel
-
-
 theorem GroupWithZero.mul_left_injective (h : x ≠ 0) :
     Function.Injective fun y => x * y := fun y y' w => by
   simpa only [← mul_assoc, inv_mul_cancel h, one_mul] using congr_arg (fun y => x⁻¹ * y) w

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -188,6 +188,26 @@ The type is required to come with an “inverse” function, and the inverse of
 class CommGroupWithZero (G₀ : Type*) extends CommMonoidWithZero G₀, GroupWithZero G₀
 #align comm_group_with_zero CommGroupWithZero
 
+section GroupWithZero
+
+variable [GroupWithZero G₀] {a b c g h x : G₀}
+
+@[simp]
+theorem mul_inv_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a :=
+  calc
+    a * b * b⁻¹ = a * (b * b⁻¹) := mul_assoc _ _ _
+    _ = a := by simp [h]
+#align mul_inv_cancel_right₀ mul_inv_cancel_right₀
+
+@[simp]
+theorem mul_inv_cancel_left₀ (h : a ≠ 0) (b : G₀) : a * (a⁻¹ * b) = b :=
+  calc
+    a * (a⁻¹ * b) = a * a⁻¹ * b := (mul_assoc _ _ _).symm
+    _ = b := by simp [h]
+#align mul_inv_cancel_left₀ mul_inv_cancel_left₀
+
+end GroupWithZero
+
 section MulZeroClass
 
 variable [MulZeroClass M₀]

Mathlib/Algebra/GroupWithZero/NeZero.lean

@@ -40,3 +40,23 @@ theorem pullback_nonzero [Zero M₀'] [One M₀'] (f : M₀' → M₀) (zero : f
     rw [zero, one]
     exact zero_ne_one⟩⟩
 #align pullback_nonzero pullback_nonzero
+
+section GroupWithZero
+
+variable [GroupWithZero G₀] {a b c g h x : G₀}
+
+-- Porting note: used `simpa` to prove `False` in lean3
+theorem inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 := fun a_eq_0 => by
+  have := mul_inv_cancel h
+  simp only [a_eq_0, mul_zero, zero_ne_one] at this
+#align inv_ne_zero inv_ne_zero
+
+@[simp]
+theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 :=
+  calc
+    a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ := by simp [inv_ne_zero h]
+    _ = a⁻¹ * a⁻¹⁻¹ := by simp [h]
+    _ = 1 := by simp [inv_ne_zero h]
+#align inv_mul_cancel inv_mul_cancel
+
+end GroupWithZero