[Merged by Bors] - chore(Data/ZMod/Basic): split ZMod.valMinAbs off

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -5,9 +5,6 @@ Authors: Aaron Anderson, Jalex Stark, Kyle Miller
 -/
 import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
 import Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
-import Mathlib.Data.Int.ModEq
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Tactic.IntervalCases
 
 /-!
 # The Friendship Theorem

Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

@@ -3,9 +3,8 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Ring.Subsemiring.Order
+import Mathlib.Data.ZMod.Basic
 
 /-!
 

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -5,12 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Algebra.CharP.Pi
 import Mathlib.Algebra.CharP.Quotient
-import Mathlib.Algebra.CharP.Two
-import Mathlib.Algebra.MvPolynomial.CommRing
-import Mathlib.Data.ZMod.Basic
-import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
-import Mathlib.LinearAlgebra.Finsupp.SumProd
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.RingTheory.MvPolynomial.Ideal
 

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Eric Wieser, Jujian Zhang
 -/
 import Mathlib.Algebra.Divisibility.Prod
+import Mathlib.Data.Fintype.Units
 import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Tactic.DeriveFintype
 
 /-!
 # A homogeneous ideal that is homogeneously prime but not prime

Counterexamples/QuadraticForm.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.QuadraticForm.Basic
-import Mathlib.Algebra.CharP.Two
-import Mathlib.Data.ZMod.Basic
 
 /-!
 # `QuadraticForm R M` and `Subtype LinearMap.IsSymm` are distinct notions in characteristic 2

Mathlib.lean

@@ -3095,6 +3095,7 @@ import Mathlib.Data.ZMod.IntUnitsPower
 import Mathlib.Data.ZMod.QuotientGroup
 import Mathlib.Data.ZMod.QuotientRing
 import Mathlib.Data.ZMod.Units
+import Mathlib.Data.ZMod.ValMinAbs
 import Mathlib.Deprecated.AlgebraClasses
 import Mathlib.Deprecated.Aliases
 import Mathlib.Deprecated.ByteArray

Mathlib/Algebra/Module/ZMod.lean

@@ -3,8 +3,6 @@ Copyright (c) 2023 Lawrence Wu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lawrence Wu
 -/
-import Mathlib.Algebra.Module.Submodule.Lattice
-import Mathlib.Data.ZMod.Basic
 import Mathlib.GroupTheory.Sylow
 
 /-!

Mathlib/Data/Nat/Defs.lean

@@ -394,6 +394,9 @@ protected lemma add_le_mul {a : ℕ} (ha : 2 ≤ a) : ∀ {b : ℕ} (_ : 2 ≤ b
 
 /-! ### `div` -/
 
+lemma le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n := by
+  rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.ofNat_mul]; rfl
+
 attribute [simp] Nat.div_self
 
 lemma div_le_iff_le_mul_add_pred (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1) := by

Mathlib/Data/Nat/Totient.lean

@@ -7,8 +7,6 @@ import Mathlib.Algebra.CharP.Two
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Data.Nat.Factorization.Induction
 import Mathlib.Data.Nat.Periodic
-import Mathlib.Data.ZMod.Basic
-import Mathlib.NumberTheory.Divisors
 
 /-!
 # Euler's totient function

Mathlib/Data/ZMod/Basic.lean

@@ -6,11 +6,10 @@ Authors: Chris Hughes
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.Algebra.Module.End
 import Mathlib.Algebra.Ring.Prod
+import Mathlib.Data.Fintype.Units
 import Mathlib.GroupTheory.GroupAction.SubMulAction
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.Tactic.FinCases
-import Mathlib.Tactic.Linarith
-import Mathlib.Data.Fintype.Units
 
 /-!
 # Integers mod `n`
@@ -26,8 +25,6 @@ Definition of the integers mod n, and the field structure on the integers mod p.
   - for `a : ZMod 0` it is the absolute value of `a`
   - for `a : ZMod n` with `0 < n` it is the least natural number in the equivalence class
 
-* `valMinAbs` returns the integer closest to zero in the equivalence class.
-
 * A coercion `cast` is defined from `ZMod n` into any ring.
 This is a ring hom if the ring has characteristic dividing `n`
 
@@ -1136,168 +1133,6 @@ theorem val_pow_le {m n : ℕ} [Fact (1 < n)] {a : ZMod n} : (a ^ m).val ≤ a.v
     apply le_trans (ZMod.val_mul_le _ _)
     apply Nat.mul_le_mul_right _ ih
 
-/-- `valMinAbs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
-  The result will be in the interval `(-n/2, n/2]`. -/
-def valMinAbs : ∀ {n : ℕ}, ZMod n → ℤ
-  | 0, x => x
-  | n@(_ + 1), x => if x.val ≤ n / 2 then x.val else (x.val : ℤ) - n
-
-@[simp]
-theorem valMinAbs_def_zero (x : ZMod 0) : valMinAbs x = x :=
-  rfl
-
-theorem valMinAbs_def_pos {n : ℕ} [NeZero n] (x : ZMod n) :
-    valMinAbs x = if x.val ≤ n / 2 then (x.val : ℤ) else x.val - n := by
-  cases n
-  · cases NeZero.ne 0 rfl
-  · rfl
-
-@[simp, norm_cast]
-theorem coe_valMinAbs : ∀ {n : ℕ} (x : ZMod n), (x.valMinAbs : ZMod n) = x
-  | 0, _ => Int.cast_id
-  | k@(n + 1), x => by
-    rw [valMinAbs_def_pos]
-    split_ifs
-    · rw [Int.cast_natCast, natCast_zmod_val]
-    · rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
-        sub_zero]
-
-theorem injective_valMinAbs {n : ℕ} : (valMinAbs : ZMod n → ℤ).Injective :=
-  Function.injective_iff_hasLeftInverse.2 ⟨_, coe_valMinAbs⟩
-
-theorem _root_.Nat.le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n := by
-  rw [Nat.le_div_iff_mul_le zero_lt_two, ← Int.ofNat_le, Int.ofNat_mul, Nat.cast_two]
-
-theorem valMinAbs_nonneg_iff {n : ℕ} [NeZero n] (x : ZMod n) : 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2 := by
-  rw [valMinAbs_def_pos]; split_ifs with h
-  · exact iff_of_true (Nat.cast_nonneg _) h
-  · exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_le h
-
-theorem valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) : a.valMinAbs * 2 = n ↔ 2 * a.val = n := by
-  cases' n with n
-  · simp
-  by_cases h : a.val ≤ n.succ / 2
-  · dsimp [valMinAbs]
-    rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm]
-  apply iff_of_false _ (mt _ h)
-  · intro he
-    rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
-    exacts [h (Nat.cast_nonneg _), zero_lt_two]
-  · rw [mul_comm]
-    exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le
-
-theorem valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) :
-    x.valMinAbs * 2 ∈ Set.Ioc (-n : ℤ) n := by
-  simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]; split_ifs with h
-  · refine ⟨(neg_lt_zero.2 <| mod_cast NeZero.pos n).trans_le (mul_nonneg ?_ ?_), h⟩
-    exacts [Nat.cast_nonneg _, zero_le_two]
-  · refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩
-    · linarith only [h]
-    · rw [sub_nonpos, Int.ofNat_le]
-      exact x.val_lt.le
-
-theorem valMinAbs_spec {n : ℕ} [NeZero n] (x : ZMod n) (y : ℤ) :
-    x.valMinAbs = y ↔ x = y ∧ y * 2 ∈ Set.Ioc (-n : ℤ) n :=
-  ⟨by
-    rintro rfl
-    exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩, fun h =>
-      by
-        rw [← sub_eq_zero]
-        apply @Int.eq_zero_of_abs_lt_dvd n
-        · rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
-        rw [← mul_lt_mul_right (@zero_lt_two ℤ _ _ _ _ _)]
-        nth_rw 1 [← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _)]
-        rw [← abs_mul, sub_mul, abs_lt]
-        constructor <;> linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]⟩
-
-theorem natAbs_valMinAbs_le {n : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs.natAbs ≤ n / 2 := by
-  rw [Nat.le_div_two_iff_mul_two_le]
-  cases' x.valMinAbs.natAbs_eq with h h
-  · rw [← h]
-    exact x.valMinAbs_mem_Ioc.2
-  · rw [← neg_le_neg_iff, ← neg_mul, ← h]
-    exact x.valMinAbs_mem_Ioc.1.le
-
-@[simp]
-theorem valMinAbs_zero : ∀ n, (0 : ZMod n).valMinAbs = 0
-  | 0 => by simp only [valMinAbs_def_zero]
-  | n + 1 => by simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]
-
-@[simp]
-theorem valMinAbs_eq_zero {n : ℕ} (x : ZMod n) : x.valMinAbs = 0 ↔ x = 0 := by
-  cases' n with n
-  · simp
-  rw [← valMinAbs_zero n.succ]
-  apply injective_valMinAbs.eq_iff
-
-theorem natCast_natAbs_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) :
-    (a.valMinAbs.natAbs : ZMod n) = if a.val ≤ (n : ℕ) / 2 then a else -a := by
-  have : (a.val : ℤ) - n ≤ 0 := by
-    rw [sub_nonpos, Int.ofNat_le]
-    exact a.val_le
-  rw [valMinAbs_def_pos]
-  split_ifs
-  · rw [Int.natAbs_ofNat, natCast_zmod_val]
-  · rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
-      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-
-@[deprecated (since := "2024-04-17")]
-alias nat_cast_natAbs_valMinAbs := natCast_natAbs_valMinAbs
-
-theorem valMinAbs_neg_of_ne_half {n : ℕ} {a : ZMod n} (ha : 2 * a.val ≠ n) :
-    (-a).valMinAbs = -a.valMinAbs := by
-  cases' eq_zero_or_neZero n with h h
-  · subst h
-    rfl
-  refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩
-  · rw [Int.cast_neg, coe_valMinAbs]
-  · rw [neg_mul, neg_lt_neg_iff]
-    exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)
-  · linarith only [a.valMinAbs_mem_Ioc.1]
-
-@[simp]
-theorem natAbs_valMinAbs_neg {n : ℕ} (a : ZMod n) : (-a).valMinAbs.natAbs = a.valMinAbs.natAbs := by
-  by_cases h2a : 2 * a.val = n
-  · rw [a.neg_eq_self_iff.2 (Or.inr h2a)]
-  · rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]
-
-theorem val_eq_ite_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) :
-    (a.val : ℤ) = a.valMinAbs + if a.val ≤ n / 2 then 0 else n := by
-  rw [valMinAbs_def_pos]
-  split_ifs <;> simp [add_zero, sub_add_cancel]
-
-theorem prime_ne_zero (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq : p ≠ q) :
-    (q : ZMod p) ≠ 0 := by
-  rwa [← Nat.cast_zero, Ne, eq_iff_modEq_nat, Nat.modEq_zero_iff_dvd, ←
-    hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]
-
-variable {n a : ℕ}
-
-theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
-    a.valMinAbs.natAbs = min a.val (n - a.val) := by
-  rw [valMinAbs_def_pos]
-  have := a.val_lt
-  omega
-
-theorem valMinAbs_natCast_of_le_half (ha : a ≤ n / 2) : (a : ZMod n).valMinAbs = a := by
-  cases n
-  · simp
-  · simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
-      ha]
-
-theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
-    (a : ZMod n).valMinAbs = a - n := by
-  cases n
-  · cases not_lt_bot ha'
-  · simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt ha', ha.not_le]
-
--- Porting note: There was an extraneous `nat_` in the mathlib3 name
-@[simp]
-theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 := by
-  refine ⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩
-  rw [← Int.natAbs_ofNat a, ← ha]
-  exact natAbs_valMinAbs_le a
-
 theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) :
     x.natAbs ≤ y.natAbs := by
   rw [intCast_eq_intCast_iff_dvd_sub] at he
@@ -1313,14 +1148,6 @@ theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (
   refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
   rw [← mul_two]; apply Nat.div_mul_le_self
 
-theorem natAbs_valMinAbs_add_le {n : ℕ} (a b : ZMod n) :
-    (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs := by
-  cases' n with n
-  · rfl
-  apply natAbs_min_of_le_div_two n.succ
-  · simp_rw [Int.cast_add, coe_valMinAbs]
-  · apply natAbs_valMinAbs_le
-
 variable (p : ℕ) [Fact p.Prime]
 
 private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 := by
@@ -1572,5 +1399,3 @@ def Nat.residueClassesEquiv (N : ℕ) [NeZero N] : ℕ ≃ ZMod N × ℕ where
         cast_id', id_eq, zero_add]
     · simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
         (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]
-
-set_option linter.style.longFile 1700

Mathlib/Data/ZMod/Units.lean

@@ -5,7 +5,6 @@ Authors: Moritz Firsching, Ashvni Narayanan, Michael Stoll
 -/
 import Mathlib.Algebra.BigOperators.Associated
 import Mathlib.Data.ZMod.Basic
-import Mathlib.Data.Nat.PrimeFin
 import Mathlib.RingTheory.Coprime.Lemmas
 
 /-!