chore: Rename nonzero_of_invertible to Invertible.ne_zero (#15860)

From LeanAPAP

Author: YaelDillies

Archive/Wiedijk100Theorems/SolutionOfCubic.lean

@@ -73,8 +73,8 @@ theorem cubic_monic_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp : p = (3 * c -
     x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
       x = s - t - b / 3 ∨ x = s * ω - t * ω ^ 2 - b / 3 ∨ x = s * ω ^ 2 - t * ω - b / 3 := by
   let y := x + b / 3
-  have hi2 : (2 : K) ≠ 0 := nonzero_of_invertible _
-  have hi3 : (3 : K) ≠ 0 := nonzero_of_invertible _
+  have hi2 : (2 : K) ≠ 0 := Invertible.ne_zero _
+  have hi3 : (3 : K) ≠ 0 := Invertible.ne_zero _
   have h9 : (9 : K) = 3 ^ 2 := by norm_num
   have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
   have h₁ : x ^ 3 + b * x ^ 2 + c * x + d = y ^ 3 + 3 * p * y - 2 * q := by
@@ -92,7 +92,7 @@ theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
     a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
       x = s - t - b / (3 * a) ∨
         x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a) := by
-  have hi3 : (3 : K) ≠ 0 := nonzero_of_invertible _
+  have hi3 : (3 : K) ≠ 0 := Invertible.ne_zero _
   have h9 : (9 : K) = 3 ^ 2 := by norm_num
   have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
   have h₁ : a * x ^ 3 + b * x ^ 2 + c * x + d
@@ -119,8 +119,8 @@ theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω
       x = s - b / (3 * a) ∨ x = s * ω - b / (3 * a) ∨ x = s * ω ^ 2 - b / (3 * a) := by
   have h₁ : ∀ x a₁ a₂ a₃ : K, x = a₁ ∨ x = a₂ ∨ x = a₃ ↔ (x - a₁) * (x - a₂) * (x - a₃) = 0 := by
     intros; simp only [mul_eq_zero, sub_eq_zero, or_assoc]
-  have hi2 : (2 : K) ≠ 0 := nonzero_of_invertible _
-  have hi3 : (3 : K) ≠ 0 := nonzero_of_invertible _
+  have hi2 : (2 : K) ≠ 0 := Invertible.ne_zero _
+  have hi3 : (3 : K) ≠ 0 := Invertible.ne_zero _
   have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
   have hb2 : b ^ 2 = 3 * a * c := by rw [sub_eq_zero] at hpz; rw [hpz]
   have hb3 : b ^ 3 = 3 * a * b * c := by rw [pow_succ, hb2]; ring

Mathlib/Algebra/CharP/Invertible.lean

@@ -28,7 +28,7 @@ def invertibleOfRingCharNotDvd {t : ℕ} (not_dvd : ¬ringChar K ∣ t) : Invert
 
 theorem not_ringChar_dvd_of_invertible {t : ℕ} [Invertible (t : K)] : ¬ringChar K ∣ t := by
   rw [← ringChar.spec, ← Ne]
-  exact nonzero_of_invertible (t : K)
+  exact Invertible.ne_zero (t : K)
 
 /-- A natural number `t` is invertible in a field `K` of characteristic `p` if `p` does not divide
 `t`. -/

Mathlib/Algebra/GroupWithZero/Invertible.lean

@@ -18,16 +18,18 @@ universe u
 
 variable {α : Type u}
 
-theorem nonzero_of_invertible [MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] : a ≠ 0 :=
+theorem Invertible.ne_zero [MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] : a ≠ 0 :=
   fun ha =>
   zero_ne_one <|
     calc
       0 = ⅟ a * a := by simp [ha]
-      _ = 1 := invOf_mul_self a
+      _ = 1 := invOf_mul_self
 
-instance (priority := 100) Invertible.ne_zero [MulZeroOneClass α] [Nontrivial α] (a : α)
+@[deprecated (since := "2024-08-15")] alias nonzero_of_invertible := Invertible.ne_zero
+
+instance (priority := 100) Invertible.toNeZero [MulZeroOneClass α] [Nontrivial α] (a : α)
     [Invertible a] : NeZero a :=
-  ⟨nonzero_of_invertible a⟩
+  ⟨Invertible.ne_zero a⟩
 
 section MonoidWithZero
 variable [MonoidWithZero α]
@@ -48,31 +50,31 @@ def invertibleOfNonzero {a : α} (h : a ≠ 0) : Invertible a :=
 
 @[simp]
 theorem invOf_eq_inv (a : α) [Invertible a] : ⅟ a = a⁻¹ :=
-  invOf_eq_right_inv (mul_inv_cancel₀ (nonzero_of_invertible a))
+  invOf_eq_right_inv (mul_inv_cancel₀ (Invertible.ne_zero a))
 
 @[simp]
 theorem inv_mul_cancel_of_invertible (a : α) [Invertible a] : a⁻¹ * a = 1 :=
-  inv_mul_cancel₀ (nonzero_of_invertible a)
+  inv_mul_cancel₀ (Invertible.ne_zero a)
 
 @[simp]
 theorem mul_inv_cancel_of_invertible (a : α) [Invertible a] : a * a⁻¹ = 1 :=
-  mul_inv_cancel₀ (nonzero_of_invertible a)
+  mul_inv_cancel₀ (Invertible.ne_zero a)
 
 /-- `a` is the inverse of `a⁻¹` -/
 def invertibleInv {a : α} [Invertible a] : Invertible a⁻¹ :=
   ⟨a, by simp, by simp⟩
 
 @[simp]
 theorem div_mul_cancel_of_invertible (a b : α) [Invertible b] : a / b * b = a :=
-  div_mul_cancel₀ a (nonzero_of_invertible b)
+  div_mul_cancel₀ a (Invertible.ne_zero b)
 
 @[simp]
 theorem mul_div_cancel_of_invertible (a b : α) [Invertible b] : a * b / b = a :=
-  mul_div_cancel_right₀ a (nonzero_of_invertible b)
+  mul_div_cancel_right₀ a (Invertible.ne_zero b)
 
 @[simp]
 theorem div_self_of_invertible (a : α) [Invertible a] : a / a = 1 :=
-  div_self (nonzero_of_invertible a)
+  div_self (Invertible.ne_zero a)
 
 /-- `b / a` is the inverse of `a / b` -/
 def invertibleDiv (a b : α) [Invertible a] [Invertible b] : Invertible (a / b) :=

Mathlib/Algebra/Ring/Invertible.lean

@@ -33,7 +33,7 @@ theorem invOf_two_add_invOf_two [NonAssocSemiring α] [Invertible (2 : α)] :
     (⅟ 2 : α) + (⅟ 2 : α) = 1 := by rw [← two_mul, mul_invOf_self]
 
 theorem pos_of_invertible_cast [Semiring α] [Nontrivial α] (n : ℕ) [Invertible (n : α)] : 0 < n :=
-  Nat.zero_lt_of_ne_zero fun h => nonzero_of_invertible (n : α) (h ▸ Nat.cast_zero)
+  Nat.zero_lt_of_ne_zero fun h => Invertible.ne_zero (n : α) (h ▸ Nat.cast_zero)
 
 theorem invOf_add_invOf [Semiring α] (a b : α) [Invertible a] [Invertible b] :
     ⅟a + ⅟b = ⅟a * (a + b) * ⅟b := by

Mathlib/LinearAlgebra/AffineSpace/Combination.lean

@@ -783,7 +783,7 @@ theorem centroid_pair [DecidableEq ι] [Invertible (2 : k)] (p : ι → P) (i₁
   · have hc : (card ({i₁, i₂} : Finset ι) : k) ≠ 0 := by
       rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
       norm_num
-      exact nonzero_of_invertible _
+      exact Invertible.ne_zero _
     rw [centroid_def,
       affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
         (sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]

Mathlib/RingTheory/WittVector/WittPolynomial.lean

@@ -229,7 +229,7 @@ theorem xInTermsOfW_vars_aux (n : ℕ) :
     n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1) := by
   apply Nat.strongInductionOn n; clear n
   intro n ih
-  rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (nonzero_of_invertible _),
+  rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (Invertible.ne_zero _),
     vars_sub_of_disjoint, vars_X, range_succ, insert_eq]
   on_goal 1 =>
     simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]

Mathlib/Tactic/NormNum/Result.lean

@@ -238,7 +238,7 @@ theorem IsRat.of_raw (α) [DivisionRing α] (n : ℤ) (d : ℕ)
   ⟨this, by simp [div_eq_mul_inv]⟩
 
 theorem IsRat.den_nz {α} [DivisionRing α] {a n d} : IsRat (a : α) n d → (d : α) ≠ 0
-  | ⟨_, _⟩ => nonzero_of_invertible (d : α)
+  | ⟨_, _⟩ => Invertible.ne_zero (d : α)
 
 /-- The result of `norm_num` running on an expression `x` of type `α`.
 Untyped version of `Result`. -/