Skip to content

Commit 755274f

Browse files
Ruben-VandeVeldeeric-wieser
Ruben-VandeVelde
and
eric-wieser
committed
feat: port Data.ZMod.Defs (#1713)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
1 parent 6e9783d commit 755274f

9 files changed

Lines changed: 195 additions & 81 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -514,7 +514,7 @@ import Mathlib.Data.Vector.Basic
514514
import Mathlib.Data.Vector.Mem
515515
import Mathlib.Data.Vector.Zip
516516
import Mathlib.Data.W.Basic
517-
import Mathlib.Data.Zmod.AdHocDefs
517+
import Mathlib.Data.ZMod.Defs
518518
import Mathlib.Deprecated.Group
519519
import Mathlib.Deprecated.Ring
520520
import Mathlib.Dynamics.FixedPoints.Basic

‎Mathlib/Data/Fintype/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -816,7 +816,7 @@ theorem Finset.toFinset_coe (s : Finset α) [Fintype (s : Set α)] : (s : Set α
816816
ext fun _ => Set.mem_toFinset
817817
#align finset.to_finset_coe Finset.toFinset_coe
818818

819-
instance (n : ℕ) : Fintype (Fin n) :=
819+
instance Fin.fintype (n : ℕ) : Fintype (Fin n) :=
820820
⟨⟨List.finRange n, List.nodup_finRange n⟩, List.mem_finRange⟩
821821

822822
theorem Fin.univ_def (n : ℕ) : (univ : Finset (Fin n)) = ⟨List.finRange n, List.nodup_finRange n⟩ :=

‎Mathlib/Data/Fintype/Card.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1023,7 +1023,7 @@ instance : Infinite ℕ :=
10231023
intro h
10241024
exact (Finset.range _).card_le_univ.not_lt ((Nat.lt_succ_self _).trans_eq (card_range _).symm)
10251025

1026-
instance : Infinite ℤ :=
1026+
instance Int.infinite : Infinite ℤ :=
10271027
Infinite.of_injective Int.ofNat fun _ _ => Int.ofNat.inj
10281028

10291029
instance [Nonempty α] : Infinite (Multiset α) :=

‎Mathlib/Data/UInt.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ import Mathlib.Data.Fin.Basic
33
import Mathlib.Algebra.Group.Defs
44
import Mathlib.Algebra.GroupWithZero.Defs
55
import Mathlib.Algebra.Ring.Basic
6-
import Mathlib.Data.Zmod.AdHocDefs
6+
import Mathlib.Data.ZMod.Defs
77

88
lemma UInt8.val_eq_of_lt {a : Nat} : a < UInt8.size -> (ofNat a).val = a := Nat.mod_eq_of_lt
99

‎Mathlib/Data/ZMod/Defs.lean‎

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
/-
2+
Copyright (c) 2022 Eric Rodriguez. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Eric Rodriguez
5+
6+
! This file was ported from Lean 3 source module data.zmod.defs
7+
! leanprover-community/mathlib commit 1126441d6bccf98c81214a0780c73d499f6721fe
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Algebra.NeZero
12+
import Mathlib.Data.Nat.ModEq
13+
import Mathlib.Data.Fintype.Lattice
14+
15+
/-!
16+
# Definition of `ZMod n` + basic results.
17+
18+
This file provides the basic details of `ZMod n`, including its commutative ring structure.
19+
20+
## Implementation details
21+
22+
This used to be inlined into `Data.ZMod.Basic`. This file imports `CharP.Basic`, which is an
23+
issue; all `CharP` instances create an `Algebra (ZMod p) R` instance; however, this instance may
24+
not be definitionally equal to other `Algebra` instances (for example, `GaloisField` also has an
25+
`Algebra` instance as it is defined as a `SplittingField`). The way to fix this is to use the
26+
forgetful inheritance pattern, and make `CharP` carry the data of what the `smul` should be (so
27+
for example, the `smul` on the `GaloisField` `CharP` instance should be equal to the `smul` from
28+
its `SplittingField` structure); there is only one possible `ZMod p` algebra for any `p`, so this
29+
is not an issue mathematically. For this to be possible, however, we need `CharP.Basic` to be
30+
able to import some part of `ZMod`.
31+
32+
-/
33+
34+
35+
namespace Fin
36+
37+
/-!
38+
## Ring structure on `Fin n`
39+
40+
We define a commutative ring structure on `Fin n`.
41+
Afterwords, when we define `ZMod n` in terms of `Fin n`, we use these definitions
42+
to register the ring structure on `ZMod n` as type class instance.
43+
-/
44+
45+
46+
open Nat.ModEq Int
47+
48+
/-- Multiplicative commutative semigroup structure on `fin n`. -/
49+
instance (n : ℕ) : CommSemigroup (Fin n) :=
50+
{ inferInstanceAs (Mul (Fin n)) with
51+
mul_assoc := fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ =>
52+
Fin.eq_of_veq
53+
(calc
54+
a * b % n * c ≡ a * b * c [MOD n] := (Nat.mod_modEq _ _).mul_right _
55+
_ ≡ a * (b * c) [MOD n] := by rw [mul_assoc]
56+
_ ≡ a * (b * c % n) [MOD n] := (Nat.mod_modEq _ _).symm.mul_left _
57+
)
58+
mul_comm := Fin.mul_comm }
59+
60+
private theorem left_distrib_aux (n : ℕ) : ∀ a b c : Fin n, a * (b + c) = a * b + a * c :=
61+
fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ =>
62+
Fin.eq_of_veq
63+
(calc
64+
a * ((b + c) % n) ≡ a * (b + c) [MOD n] := (Nat.mod_modEq _ _).mul_left _
65+
_ ≡ a * b + a * c [MOD n] := by rw [mul_add]
66+
_ ≡ a * b % n + a * c % n [MOD n] := (Nat.mod_modEq _ _).symm.add (Nat.mod_modEq _ _).symm
67+
)
68+
69+
/-- Commutative ring structure on `Fin n`. -/
70+
instance (n : ℕ) [NeZero n] : CommRing (Fin n) :=
71+
{ Fin.instAddMonoidWithOneFin n, Fin.addCommGroup n,
72+
Fin.instCommSemigroupFin n with
73+
one_mul := Fin.one_mul
74+
mul_one := Fin.mul_one
75+
left_distrib := left_distrib_aux n
76+
right_distrib := fun a b c => by
77+
rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm],
78+
-- porting note: new, see
79+
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring.20vs.20Ring/near/322876462
80+
zero_mul := Fin.zero_mul
81+
mul_zero := Fin.mul_zero }
82+
83+
end Fin
84+
85+
/-- The integers modulo `n : ℕ`. -/
86+
def ZMod : ℕ → Type
87+
| 0 => ℤ
88+
| n + 1 => Fin (n + 1)
89+
#align zmod ZMod
90+
91+
instance ZMod.decidableEq : ∀ n : ℕ, DecidableEq (ZMod n)
92+
| 0 => by dsimp [ZMod]; infer_instance
93+
| n + 1 => by dsimp [ZMod]; infer_instance
94+
#align zmod.decidable_eq ZMod.decidableEq
95+
96+
instance ZMod.repr : ∀ n : ℕ, Repr (ZMod n)
97+
| 0 => by dsimp [ZMod]; infer_instance
98+
| n + 1 => by dsimp [ZMod]; infer_instance
99+
#align zmod.has_repr ZMod.repr
100+
101+
namespace ZMod
102+
103+
instance fintype : ∀ (n : ℕ) [NeZero n], Fintype (ZMod n)
104+
| 0, h => (h.ne rfl).elim
105+
| n + 1, _ => Fin.fintype (n + 1)
106+
#align zmod.fintype ZMod.fintype
107+
108+
instance infinite : Infinite (ZMod 0) :=
109+
Int.infinite
110+
#align zmod.infinite ZMod.infinite
111+
112+
@[simp]
113+
theorem card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n := by
114+
cases n with
115+
| zero => exact (not_finite (ZMod 0)).elim
116+
| succ n => convert Fintype.card_fin (n + 1); apply Subsingleton.elim
117+
#align zmod.card ZMod.card
118+
119+
/- We define each field by cases, to ensure that the eta-expanded `ZMod.commRing` is defeq to the
120+
original, this helps avoid diamonds with instances coming from classes extending `CommRing` such as
121+
field. -/
122+
instance commRing (n : ℕ) : CommRing (ZMod n) where
123+
add := Nat.casesOn n (@Add.add Int _) fun n => @Add.add (Fin n.succ) _
124+
add_assoc := Nat.casesOn n (@add_assoc Int _) fun n => @add_assoc (Fin n.succ) _
125+
zero := Nat.casesOn n (0 : Int) fun n => (0 : Fin n.succ)
126+
zero_add := Nat.casesOn n (@zero_add Int _) fun n => @zero_add (Fin n.succ) _
127+
add_zero := Nat.casesOn n (@add_zero Int _) fun n => @add_zero (Fin n.succ) _
128+
neg := Nat.casesOn n (@Neg.neg Int _) fun n => @Neg.neg (Fin n.succ) _
129+
sub := Nat.casesOn n (@Sub.sub Int _) fun n => @Sub.sub (Fin n.succ) _
130+
sub_eq_add_neg := Nat.casesOn n (@sub_eq_add_neg Int _) fun n => @sub_eq_add_neg (Fin n.succ) _
131+
zsmul := Nat.casesOn n
132+
(inferInstanceAs (CommRing ℤ)).zsmul fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul
133+
zsmul_zero' := Nat.casesOn n
134+
(inferInstanceAs (CommRing ℤ)).zsmul_zero'
135+
fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul_zero'
136+
zsmul_succ' := Nat.casesOn n
137+
(inferInstanceAs (CommRing ℤ)).zsmul_succ'
138+
fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul_succ'
139+
zsmul_neg' := Nat.casesOn n
140+
(inferInstanceAs (CommRing ℤ)).zsmul_neg'
141+
fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul_neg'
142+
nsmul := Nat.casesOn n
143+
(inferInstanceAs (CommRing ℤ)).nsmul fun n => (inferInstanceAs (CommRing (Fin n.succ))).nsmul
144+
nsmul_zero := Nat.casesOn n
145+
(inferInstanceAs (CommRing ℤ)).nsmul_zero
146+
fun n => (inferInstanceAs (CommRing (Fin n.succ))).nsmul_zero
147+
nsmul_succ := Nat.casesOn n
148+
(inferInstanceAs (CommRing ℤ)).nsmul_succ
149+
fun n => (inferInstanceAs (CommRing (Fin n.succ))).nsmul_succ
150+
-- porting note: `match` didn't work here
151+
add_left_neg := Nat.casesOn n (@add_left_neg Int _) fun n => @add_left_neg (Fin n.succ) _
152+
add_comm := Nat.casesOn n (@add_comm Int _) fun n => @add_comm (Fin n.succ) _
153+
mul := Nat.casesOn n (@Mul.mul Int _) fun n => @Mul.mul (Fin n.succ) _
154+
mul_assoc := Nat.casesOn n (@mul_assoc Int _) fun n => @mul_assoc (Fin n.succ) _
155+
one := Nat.casesOn n (1 : Int) fun n => (1 : Fin n.succ)
156+
one_mul := Nat.casesOn n (@one_mul Int _) fun n => @one_mul (Fin n.succ) _
157+
mul_one := Nat.casesOn n (@mul_one Int _) fun n => @mul_one (Fin n.succ) _
158+
natCast := Nat.casesOn n ((↑) : ℕ → ℤ) fun n => ((↑) : ℕ → Fin n.succ)
159+
natCast_zero := Nat.casesOn n (@Nat.cast_zero Int _) fun n => @Nat.cast_zero (Fin n.succ) _
160+
natCast_succ := Nat.casesOn n (@Nat.cast_succ Int _) fun n => @Nat.cast_succ (Fin n.succ) _
161+
intCast := Nat.casesOn n ((↑) : ℤ → ℤ) fun n => ((↑) : ℤ → Fin n.succ)
162+
intCast_ofNat := Nat.casesOn n (@Int.cast_ofNat Int _) fun n => @Int.cast_ofNat (Fin n.succ) _
163+
intCast_negSucc :=
164+
Nat.casesOn n (@Int.cast_negSucc Int _) fun n => @Int.cast_negSucc (Fin n.succ) _
165+
left_distrib := Nat.casesOn n (@left_distrib Int _ _ _) fun n => @left_distrib (Fin n.succ) _ _ _
166+
right_distrib :=
167+
Nat.casesOn n (@right_distrib Int _ _ _) fun n => @right_distrib (Fin n.succ) _ _ _
168+
mul_comm := Nat.casesOn n (@mul_comm Int _) fun n => @mul_comm (Fin n.succ) _
169+
-- porting note: new, see
170+
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring.20vs.20Ring/near/322876462
171+
zero_mul := Nat.casesOn n (@zero_mul Int _) fun n => @zero_mul (Fin n.succ) _
172+
mul_zero := Nat.casesOn n (@mul_zero Int _) fun n => @mul_zero (Fin n.succ) _
173+
-- porting note: all npow fields are new, but probably should be backported
174+
npow := Nat.casesOn n
175+
(inferInstanceAs (CommRing ℤ)).npow fun n => (inferInstanceAs (CommRing (Fin n.succ))).npow
176+
npow_zero := Nat.casesOn n
177+
(inferInstanceAs (CommRing ℤ)).npow_zero
178+
fun n => (inferInstanceAs (CommRing (Fin n.succ))).npow_zero
179+
npow_succ := Nat.casesOn n
180+
(inferInstanceAs (CommRing ℤ)).npow_succ
181+
fun n => (inferInstanceAs (CommRing (Fin n.succ))).npow_succ
182+
#align zmod.comm_ring ZMod.commRing
183+
184+
instance inhabited (n : ℕ) : Inhabited (ZMod n) :=
185+
⟨0⟩
186+
#align zmod.inhabited ZMod.inhabited
187+
188+
end ZMod

‎Mathlib/Data/Zmod/AdHocDefs.lean‎

Lines changed: 0 additions & 72 deletions
This file was deleted.

‎Mathlib/Logic/Basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -93,13 +93,13 @@ Certain propositions should not be treated as a class globally,
9393
but sometimes it is very convenient to be able to use the type class system
9494
in specific circumstances.
9595
96-
For example, `Zmod p` is a field if and only if `p` is a prime number.
96+
For example, `ZMod p` is a field if and only if `p` is a prime number.
9797
In order to be able to find this field instance automatically by type class search,
9898
we have to turn `p.prime` into an instance implicit assumption.
9999
100100
On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
101101
and it is questionable whether making `Nat.prime` a class is desirable at all.
102-
The compromise is to add the assumption `[Fact p.prime]` to `Zmod.field`.
102+
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.
103103
104104
In particular, this class is not intended for turning the type class system
105105
into an automated theorem prover for first order logic. -/

‎scripts/start_port.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ git add "$mathlib4_path"
6262
git commit -m 'Initial file copy from mathport'
6363

6464
sed -i 's/Mathbin\./Mathlib\./g' "$mathlib4_path"
65-
sed -i '/^import/{s/[.]Smul/.SMul/g; s/[.]Pnat/.PNat/g; s/[.]Gcd/.GCD/g; s/[.]Modeq/.ModEq/g}' "$mathlib4_path"
65+
sed -i '/^import/{s/[.]Smul/.SMul/g; s/[.]Pnat/.PNat/g; s/[.]Gcd/.GCD/g; s/[.]Modeq/.ModEq/g; s/[.]Zmod/.ZMod/g}' "$mathlib4_path"
6666

6767
# awk script taken from https://github.com/leanprover-community/mathlib4/pull/1523
6868
awk '{do {{if (match($0, "^ by$") && length(p) < 98 && (!(match(p, "^[ \t]*--.*$")))) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}' "$mathlib4_path" > "$mathlib4_path.tmp"

‎scripts/style-exceptions.txt‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,8 +71,6 @@ Mathlib/Data/UInt.lean : line 5 : ERR_COP : Malformed or missing copyright heade
7171
Mathlib/Data/UInt.lean : line 7 : ERR_COP : Malformed or missing copyright header
7272
Mathlib/Data/UInt.lean : line 7 : ERR_MOD : Module docstring missing, or too late
7373
Mathlib/Data/UnionFind.lean : line 10 : ERR_MOD : Module docstring missing, or too late
74-
Mathlib/Data/Zmod/AdHocDefs.lean : line 0 : ERR_COP : Malformed or missing copyright header
75-
Mathlib/Data/Zmod/AdHocDefs.lean : line 2 : ERR_COP : Malformed or missing copyright header
7674
Mathlib/Init/Algebra/Functions.lean : line 9 : ERR_MOD : Module docstring missing, or too late
7775
Mathlib/Init/Data/Int/Basic.lean : line 13 : ERR_MOD : Module docstring missing, or too late
7876
Mathlib/Init/Data/Nat/Basic.lean : line 7 : ERR_MOD : Module docstring missing, or too late

0 commit comments

Comments
 (0)