Skip to content

Commit 74bf56f

Browse files
YaelDilliesYaelDillies
committed
chore(Data/ZMod/Basic): split ZMod.valMinAbs off (#21308)
1 parent 05f71fa commit 74bf56f

23 files changed

Lines changed: 191 additions & 219 deletions

File tree

‎Archive/Wiedijk100Theorems/FriendshipGraphs.lean‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,6 @@ Authors: Aaron Anderson, Jalex Stark, Kyle Miller
55
-/
66
import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
77
import Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
8-
import Mathlib.Data.Int.ModEq
9-
import Mathlib.Data.ZMod.Basic
10-
import Mathlib.Tactic.IntervalCases
118

129
/-!
1310
# The Friendship Theorem

‎Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,8 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Damiano Testa
55
-/
6-
import Mathlib.Data.ZMod.Basic
7-
import Mathlib.Algebra.Order.Monoid.Basic
86
import Mathlib.Algebra.Ring.Subsemiring.Order
7+
import Mathlib.Data.ZMod.Basic
98

109
/-!
1110

‎Counterexamples/CliffordAlgebraNotInjective.lean‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,7 @@ Authors: Eric Wieser
55
-/
66
import Mathlib.Algebra.CharP.Pi
77
import Mathlib.Algebra.CharP.Quotient
8-
import Mathlib.Algebra.CharP.Two
9-
import Mathlib.Algebra.MvPolynomial.CommRing
10-
import Mathlib.Data.ZMod.Basic
11-
import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
128
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
13-
import Mathlib.LinearAlgebra.Finsupp.SumProd
149
import Mathlib.RingTheory.MvPolynomial.Basic
1510
import Mathlib.RingTheory.MvPolynomial.Ideal
1611

‎Counterexamples/HomogeneousPrimeNotPrime.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin, Eric Wieser, Jujian Zhang
55
-/
66
import Mathlib.Algebra.Divisibility.Prod
7+
import Mathlib.Data.Fintype.Units
78
import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
8-
import Mathlib.Data.ZMod.Basic
9-
import Mathlib.Tactic.DeriveFintype
109

1110
/-!
1211
# A homogeneous ideal that is homogeneously prime but not prime

‎Counterexamples/QuadraticForm.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Wieser
55
-/
66
import Mathlib.LinearAlgebra.QuadraticForm.Basic
7-
import Mathlib.Algebra.CharP.Two
8-
import Mathlib.Data.ZMod.Basic
97

108
/-!
119
# `QuadraticForm R M` and `Subtype LinearMap.IsSymm` are distinct notions in characteristic 2

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3095,6 +3095,7 @@ import Mathlib.Data.ZMod.IntUnitsPower
30953095
import Mathlib.Data.ZMod.QuotientGroup
30963096
import Mathlib.Data.ZMod.QuotientRing
30973097
import Mathlib.Data.ZMod.Units
3098+
import Mathlib.Data.ZMod.ValMinAbs
30983099
import Mathlib.Deprecated.AlgebraClasses
30993100
import Mathlib.Deprecated.Aliases
31003101
import Mathlib.Deprecated.ByteArray

‎Mathlib/Algebra/Module/ZMod.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@ Copyright (c) 2023 Lawrence Wu. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Lawrence Wu
55
-/
6-
import Mathlib.Algebra.Module.Submodule.Lattice
7-
import Mathlib.Data.ZMod.Basic
86
import Mathlib.GroupTheory.Sylow
97

108
/-!

‎Mathlib/Data/Nat/Defs.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -394,6 +394,9 @@ protected lemma add_le_mul {a : ℕ} (ha : 2 ≤ a) : ∀ {b : ℕ} (_ : 2 ≤ b
394394

395395
/-! ### `div` -/
396396

397+
lemma le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n := by
398+
rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.ofNat_mul]; rfl
399+
397400
attribute [simp] Nat.div_self
398401

399402
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‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@ import Mathlib.Algebra.CharP.Two
77
import Mathlib.Data.Nat.Factorization.Basic
88
import Mathlib.Data.Nat.Factorization.Induction
99
import Mathlib.Data.Nat.Periodic
10-
import Mathlib.Data.ZMod.Basic
11-
import Mathlib.NumberTheory.Divisors
1210

1311
/-!
1412
# Euler's totient function

‎Mathlib/Data/ZMod/Basic.lean‎

Lines changed: 1 addition & 176 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,10 @@ Authors: Chris Hughes
66
import Mathlib.Algebra.CharP.Basic
77
import Mathlib.Algebra.Module.End
88
import Mathlib.Algebra.Ring.Prod
9+
import Mathlib.Data.Fintype.Units
910
import Mathlib.GroupTheory.GroupAction.SubMulAction
1011
import Mathlib.GroupTheory.OrderOfElement
1112
import Mathlib.Tactic.FinCases
12-
import Mathlib.Tactic.Linarith
13-
import Mathlib.Data.Fintype.Units
1413

1514
/-!
1615
# Integers mod `n`
@@ -26,8 +25,6 @@ Definition of the integers mod n, and the field structure on the integers mod p.
2625
- for `a : ZMod 0` it is the absolute value of `a`
2726
- for `a : ZMod n` with `0 < n` it is the least natural number in the equivalence class
2827
29-
* `valMinAbs` returns the integer closest to zero in the equivalence class.
30-
3128
* A coercion `cast` is defined from `ZMod n` into any ring.
3229
This is a ring hom if the ring has characteristic dividing `n`
3330
@@ -1136,168 +1133,6 @@ theorem val_pow_le {m n : ℕ} [Fact (1 < n)] {a : ZMod n} : (a ^ m).val ≤ a.v
11361133
apply le_trans (ZMod.val_mul_le _ _)
11371134
apply Nat.mul_le_mul_right _ ih
11381135

1139-
/-- `valMinAbs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
1140-
The result will be in the interval `(-n/2, n/2]`. -/
1141-
def valMinAbs : ∀ {n : ℕ}, ZMod n → ℤ
1142-
| 0, x => x
1143-
| n@(_ + 1), x => if x.val ≤ n / 2 then x.val else (x.val : ℤ) - n
1144-
1145-
@[simp]
1146-
theorem valMinAbs_def_zero (x : ZMod 0) : valMinAbs x = x :=
1147-
rfl
1148-
1149-
theorem valMinAbs_def_pos {n : ℕ} [NeZero n] (x : ZMod n) :
1150-
valMinAbs x = if x.val ≤ n / 2 then (x.val : ℤ) else x.val - n := by
1151-
cases n
1152-
· cases NeZero.ne 0 rfl
1153-
· rfl
1154-
1155-
@[simp, norm_cast]
1156-
theorem coe_valMinAbs : ∀ {n : ℕ} (x : ZMod n), (x.valMinAbs : ZMod n) = x
1157-
| 0, _ => Int.cast_id
1158-
| k@(n + 1), x => by
1159-
rw [valMinAbs_def_pos]
1160-
split_ifs
1161-
· rw [Int.cast_natCast, natCast_zmod_val]
1162-
· rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
1163-
sub_zero]
1164-
1165-
theorem injective_valMinAbs {n : ℕ} : (valMinAbs : ZMod n → ℤ).Injective :=
1166-
Function.injective_iff_hasLeftInverse.2 ⟨_, coe_valMinAbs⟩
1167-
1168-
theorem _root_.Nat.le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n := by
1169-
rw [Nat.le_div_iff_mul_le zero_lt_two, ← Int.ofNat_le, Int.ofNat_mul, Nat.cast_two]
1170-
1171-
theorem valMinAbs_nonneg_iff {n : ℕ} [NeZero n] (x : ZMod n) : 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2 := by
1172-
rw [valMinAbs_def_pos]; split_ifs with h
1173-
· exact iff_of_true (Nat.cast_nonneg _) h
1174-
· exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_le h
1175-
1176-
theorem valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) : a.valMinAbs * 2 = n ↔ 2 * a.val = n := by
1177-
cases' n with n
1178-
· simp
1179-
by_cases h : a.val ≤ n.succ / 2
1180-
· dsimp [valMinAbs]
1181-
rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm]
1182-
apply iff_of_false _ (mt _ h)
1183-
· intro he
1184-
rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
1185-
exacts [h (Nat.cast_nonneg _), zero_lt_two]
1186-
· rw [mul_comm]
1187-
exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le
1188-
1189-
theorem valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) :
1190-
x.valMinAbs * 2 ∈ Set.Ioc (-n : ℤ) n := by
1191-
simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]; split_ifs with h
1192-
· refine ⟨(neg_lt_zero.2 <| mod_cast NeZero.pos n).trans_le (mul_nonneg ?_ ?_), h⟩
1193-
exacts [Nat.cast_nonneg _, zero_le_two]
1194-
· refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩
1195-
· linarith only [h]
1196-
· rw [sub_nonpos, Int.ofNat_le]
1197-
exact x.val_lt.le
1198-
1199-
theorem valMinAbs_spec {n : ℕ} [NeZero n] (x : ZMod n) (y : ℤ) :
1200-
x.valMinAbs = y ↔ x = y ∧ y * 2 ∈ Set.Ioc (-n : ℤ) n :=
1201-
⟨by
1202-
rintro rfl
1203-
exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩, fun h =>
1204-
by
1205-
rw [← sub_eq_zero]
1206-
apply @Int.eq_zero_of_abs_lt_dvd n
1207-
· rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
1208-
rw [← mul_lt_mul_right (@zero_lt_two ℤ _ _ _ _ _)]
1209-
nth_rw 1 [← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _)]
1210-
rw [← abs_mul, sub_mul, abs_lt]
1211-
constructor <;> linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]⟩
1212-
1213-
theorem natAbs_valMinAbs_le {n : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs.natAbs ≤ n / 2 := by
1214-
rw [Nat.le_div_two_iff_mul_two_le]
1215-
cases' x.valMinAbs.natAbs_eq with h h
1216-
· rw [← h]
1217-
exact x.valMinAbs_mem_Ioc.2
1218-
· rw [← neg_le_neg_iff, ← neg_mul, ← h]
1219-
exact x.valMinAbs_mem_Ioc.1.le
1220-
1221-
@[simp]
1222-
theorem valMinAbs_zero : ∀ n, (0 : ZMod n).valMinAbs = 0
1223-
| 0 => by simp only [valMinAbs_def_zero]
1224-
| n + 1 => by simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]
1225-
1226-
@[simp]
1227-
theorem valMinAbs_eq_zero {n : ℕ} (x : ZMod n) : x.valMinAbs = 0 ↔ x = 0 := by
1228-
cases' n with n
1229-
· simp
1230-
rw [← valMinAbs_zero n.succ]
1231-
apply injective_valMinAbs.eq_iff
1232-
1233-
theorem natCast_natAbs_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) :
1234-
(a.valMinAbs.natAbs : ZMod n) = if a.val ≤ (n : ℕ) / 2 then a else -a := by
1235-
have : (a.val : ℤ) - n ≤ 0 := by
1236-
rw [sub_nonpos, Int.ofNat_le]
1237-
exact a.val_le
1238-
rw [valMinAbs_def_pos]
1239-
split_ifs
1240-
· rw [Int.natAbs_ofNat, natCast_zmod_val]
1241-
· rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
1242-
Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
1243-
1244-
@[deprecated (since := "2024-04-17")]
1245-
alias nat_cast_natAbs_valMinAbs := natCast_natAbs_valMinAbs
1246-
1247-
theorem valMinAbs_neg_of_ne_half {n : ℕ} {a : ZMod n} (ha : 2 * a.val ≠ n) :
1248-
(-a).valMinAbs = -a.valMinAbs := by
1249-
cases' eq_zero_or_neZero n with h h
1250-
· subst h
1251-
rfl
1252-
refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩
1253-
· rw [Int.cast_neg, coe_valMinAbs]
1254-
· rw [neg_mul, neg_lt_neg_iff]
1255-
exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)
1256-
· linarith only [a.valMinAbs_mem_Ioc.1]
1257-
1258-
@[simp]
1259-
theorem natAbs_valMinAbs_neg {n : ℕ} (a : ZMod n) : (-a).valMinAbs.natAbs = a.valMinAbs.natAbs := by
1260-
by_cases h2a : 2 * a.val = n
1261-
· rw [a.neg_eq_self_iff.2 (Or.inr h2a)]
1262-
· rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]
1263-
1264-
theorem val_eq_ite_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) :
1265-
(a.val : ℤ) = a.valMinAbs + if a.val ≤ n / 2 then 0 else n := by
1266-
rw [valMinAbs_def_pos]
1267-
split_ifs <;> simp [add_zero, sub_add_cancel]
1268-
1269-
theorem prime_ne_zero (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq : p ≠ q) :
1270-
(q : ZMod p) ≠ 0 := by
1271-
rwa [← Nat.cast_zero, Ne, eq_iff_modEq_nat, Nat.modEq_zero_iff_dvd, ←
1272-
hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]
1273-
1274-
variable {n a : ℕ}
1275-
1276-
theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
1277-
a.valMinAbs.natAbs = min a.val (n - a.val) := by
1278-
rw [valMinAbs_def_pos]
1279-
have := a.val_lt
1280-
omega
1281-
1282-
theorem valMinAbs_natCast_of_le_half (ha : a ≤ n / 2) : (a : ZMod n).valMinAbs = a := by
1283-
cases n
1284-
· simp
1285-
· simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
1286-
ha]
1287-
1288-
theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
1289-
(a : ZMod n).valMinAbs = a - n := by
1290-
cases n
1291-
· cases not_lt_bot ha'
1292-
· simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt ha', ha.not_le]
1293-
1294-
-- Porting note: There was an extraneous `nat_` in the mathlib3 name
1295-
@[simp]
1296-
theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 := by
1297-
refine ⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩
1298-
rw [← Int.natAbs_ofNat a, ← ha]
1299-
exact natAbs_valMinAbs_le a
1300-
13011136
theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) :
13021137
x.natAbs ≤ y.natAbs := by
13031138
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) (
13131148
refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
13141149
rw [← mul_two]; apply Nat.div_mul_le_self
13151150

1316-
theorem natAbs_valMinAbs_add_le {n : ℕ} (a b : ZMod n) :
1317-
(a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs := by
1318-
cases' n with n
1319-
· rfl
1320-
apply natAbs_min_of_le_div_two n.succ
1321-
· simp_rw [Int.cast_add, coe_valMinAbs]
1322-
· apply natAbs_valMinAbs_le
1323-
13241151
variable (p : ℕ) [Fact p.Prime]
13251152

13261153
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
15721399
cast_id', id_eq, zero_add]
15731400
· simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
15741401
(Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]
1575-
1576-
set_option linter.style.longFile 1700

0 commit comments

Comments
 (0)