modEq_iff_dvd_subtheoremApplies a library theorempropext, Quot.sound
modEq_iff_dvd_subLean 4Applies a library theoremFormally verified
/-- **The definition used in the lesson.** `a ≡ b (mod n)` means `n ∣ a - b`. Mathlib defines`a ≡ b [ZMOD n]` as "same remainder", `a % n = b % n`; its theorem `Int.modEq_iff_dvd`(`n ∣ b - a`) shows the two definitions agree. -/theorem modEq_iff_dvd_sub {n a b : ℤ} : a ≡ b [ZMOD n] ↔ n ∣ a - b := Int.modEq_iff_dvd.trans dvd_sub_comm
modEq_equivalencetheoremProved here from basic factspropext, Quot.sound
modEq_equivalenceLean 4Proved here from basic factsFormally verified
/-- **Congruence modulo `n` is an equivalence relation.** Reflexive: `n ∣ 0 = a - a`.Symmetric: `b - a = -(a - b)`. Transitive: `a - c = (a - b) + (b - c)`. -/theorem modEq_equivalence (n : ℤ) : Equivalence (Int.ModEq n) where refl a := modEq_iff_dvd_sub.mpr (by simp) symm {a b} h := by rw [modEq_iff_dvd_sub] at h ⊢ have h' : n ∣ -(a - b) := dvd_neg.mpr h rwa [neg_sub] at h' trans {a b c} h₁ h₂ := by rw [modEq_iff_dvd_sub] at h₁ h₂ ⊢ have h : n ∣ (a - b) + (b - c) := dvd_add h₁ h₂ rwa [sub_add_sub_cancel] at h
modEq_addtheoremProved here from basic factspropext, Quot.sound
modEq_addLean 4Proved here from basic factsFormally verified
/-- **Congruences can be added.** If `a ≡ b` and `c ≡ d (mod n)` then `a + c ≡ b + d`, because`(a + c) - (b + d) = (a - b) + (c - d)`. -/theorem modEq_add {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] := by rw [modEq_iff_dvd_sub] at h₁ h₂ ⊢ have h : (a + c) - (b + d) = (a - b) + (c - d) := by ring rw [h] exact dvd_add h₁ h₂
modEq_multheoremProved here from basic factspropext, Quot.sound
modEq_mulLean 4Proved here from basic factsFormally verified
/-- **Congruences can be multiplied.** If `a ≡ b` and `c ≡ d (mod n)` then `ac ≡ bd`, because`ac - bd = a(c - d) + d(a - b)` and `n` divides both terms. -/theorem modEq_mul {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] := by rw [modEq_iff_dvd_sub] at h₁ h₂ ⊢ have h : a * c - b * d = a * (c - d) + d * (a - b) := by ring rw [h] exact dvd_add (dvd_mul_of_dvd_right h₂ a) (dvd_mul_of_dvd_right h₁ d)
exists_inverse_iff_isCoprimetheoremProved here from basic factspropext, Classical.choice, Quot.sound
exists_inverse_iff_isCoprimeLean 4Proved here from basic factsFormally verified
/-- **`a` has an inverse modulo `n` exactly when `a` and `n` are coprime**, in Bézout's form:`ab ≡ 1 (mod n)` for some `b` if and only if `ua + vn = 1` for some integers `u, v`(Mathlib's `IsCoprime a n`).* (→) If `n ∣ ab - 1`, say `ab - 1 = nk`, then `b · a + (-k) · n = 1`.* (←) If `ua + vn = 1` then `au - 1 = -vn` is a multiple of `n`, so `u` is an inverse. -/theorem exists_inverse_iff_isCoprime {a n : ℤ} : (∃ b, a * b ≡ 1 [ZMOD n]) ↔ IsCoprime a n := by constructor · rintro ⟨b, hb⟩ obtain ⟨k, hk⟩ := modEq_iff_dvd_sub.mp hb exact ⟨b, -k, by linear_combination hk⟩ · rintro ⟨u, v, huv⟩ refine ⟨u, modEq_iff_dvd_sub.mpr ⟨-v, ?_⟩⟩ linear_combination huv
exists_inverse_iff_gcdtheoremProved here from basic factspropext, Classical.choice, Quot.sound
exists_inverse_iff_gcdLean 4Proved here from basic factsFormally verified
/-- The same criterion with the gcd: `a` is invertible modulo `n` if and only if`gcd(a, n) = 1`. This combines `exists_inverse_iff_isCoprime` with Mathlib's`Int.isCoprime_iff_gcd_eq_one` (Bézout's identity and its converse). -/theorem exists_inverse_iff_gcd {a n : ℤ} : (∃ b, a * b ≡ 1 [ZMOD n]) ↔ Int.gcd a n = 1 := exists_inverse_iff_isCoprime.trans Int.isCoprime_iff_gcd_eq_one
cancel_of_isCoprimetheoremProved here from basic factspropext, Classical.choice, Quot.sound
cancel_of_isCoprimeLean 4Proved here from basic factsFormally verified
/-- **Cancelling a coprime factor is allowed.** If `c` is invertible modulo `n` and`ca ≡ cb`, multiply both sides by an inverse `u` of `c`: `a ≡ (uc)a = u(ca) ≡ u(cb) = (uc)b ≡ b`. -/theorem cancel_of_isCoprime {n a b c : ℤ} (hc : IsCoprime c n) (h : c * a ≡ c * b [ZMOD n]) : a ≡ b [ZMOD n] := by obtain ⟨u, hu⟩ := exists_inverse_iff_isCoprime.mpr hc have hu' : u * c ≡ 1 [ZMOD n] := by rwa [mul_comm] at hu have ha : u * c * a ≡ 1 * a [ZMOD n] := modEq_mul hu' (Int.ModEq.refl a) have hb : u * c * b ≡ 1 * b [ZMOD n] := modEq_mul hu' (Int.ModEq.refl b) have hab : u * (c * a) ≡ u * (c * b) [ZMOD n] := modEq_mul (Int.ModEq.refl u) h rw [one_mul] at ha hb rw [← mul_assoc, ← mul_assoc] at hab exact (ha.symm.trans hab).trans hb
crt_existstheoremProved here from basic factspropext, Classical.choice, Quot.sound
crt_existsLean 4Proved here from basic factsFormally verified
/-- **Chinese remainder theorem, existence.** If `um + vn = 1`, then `x = a·vn + b·um` solves`x ≡ a (mod m)` and `x ≡ b (mod n)`: modulo `m` we have `vn = 1 - um ≡ 1`, and modulo `n` we have`um ≡ 1`. Each congruence is checked by exhibiting the quotient. -/theorem crt_exists {m n : ℤ} (h : IsCoprime m n) (a b : ℤ) : ∃ x, x ≡ a [ZMOD m] ∧ x ≡ b [ZMOD n] := by obtain ⟨u, v, huv⟩ := h refine ⟨a * v * n + b * u * m, ?_, ?_⟩ · exact modEq_iff_dvd_sub.mpr ⟨b * u - a * u, by linear_combination a * huv⟩ · exact modEq_iff_dvd_sub.mpr ⟨a * v - b * v, by linear_combination b * huv⟩
crt_uniquetheoremProved here from basic factspropext, Quot.sound
crt_uniqueLean 4Proved here from basic factsFormally verified
/-- **Chinese remainder theorem, uniqueness.** If `m, n` are coprime and `x ≡ y` modulo both`m` and `n`, then `x ≡ y (mod mn)`: `m` and `n` both divide `x - y`, and coprime divisorsmultiply (Mathlib's `IsCoprime.mul_dvd`, itself proved from Bézout). -/theorem crt_unique {m n x y : ℤ} (h : IsCoprime m n) (hm : x ≡ y [ZMOD m]) (hn : x ≡ y [ZMOD n]) : x ≡ y [ZMOD m * n] := modEq_iff_dvd_sub.mpr (h.mul_dvd (modEq_iff_dvd_sub.mp hm) (modEq_iff_dvd_sub.mp hn))
pow_prime_eq_selftheoremProved here from basic factspropext, Classical.choice, Quot.sound
pow_prime_eq_selfLean 4Proved here from basic factsFormally verified
/-- **Fermat's little theorem, first form: `aᵖ ≡ a (mod p)` for every `a`.** In `ZMod p` thisreads `xᵖ = x`. Proof by induction on `a`, as in the lesson: `0ᵖ = 0`, and`(a + 1)ᵖ = aᵖ + 1ᵖ` because `p` divides every binomial coefficient `C(p, k)` with `0 < k < p`(Mathlib's `add_pow_char`, "the freshman's dream" in characteristic `p`). Every residue is theimage of a natural number, which finishes the proof. -/theorem pow_prime_eq_self (p : ℕ) [Fact p.Prime] (x : ZMod p) : x ^ p = x := by have key : ∀ k : ℕ, (k : ZMod p) ^ p = k := by intro k induction k with | zero => simp [zero_pow (Fact.out : p.Prime).ne_zero] | succ k ih => rw [Nat.cast_succ, add_pow_char, ih, one_pow] obtain ⟨k, rfl⟩ := ZMod.natCast_zmod_surjective x exact key k
fermat_littletheoremProved here from basic factspropext, Classical.choice, Quot.sound
fermat_littleLean 4Proved here from basic factsFormally verified
/-- **Fermat's little theorem: if `p ∤ a` then `aᵖ⁻¹ ≡ 1 (mod p)`.** From `a · aᵖ⁻¹ = aᵖ = a`we may cancel `a ≠ 0`, because `ZMod p` is a field. -/theorem fermat_little (p : ℕ) [Fact p.Prime] {a : ZMod p} (ha : a ≠ 0) : a ^ (p - 1) = 1 := by have hp : 1 ≤ p := (Fact.out : p.Prime).one_lt.le have h : a * a ^ (p - 1) = a * 1 := by rw [← pow_succ', Nat.sub_add_cancel hp, pow_prime_eq_self, mul_one] exact mul_left_cancel₀ ha h
fermat_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
fermat_libraryLean 4Applies a library theoremFormally verified
/-- Fermat's little theorem for integers, from Mathlib (`Int.ModEq.pow_card_sub_one_eq_one`):if `p` is prime and `a` is coprime to `p`, then `aᵖ⁻¹ ≡ 1 (mod p)`. -/theorem fermat_library {p : ℕ} (hp : p.Prime) {a : ℤ} (ha : IsCoprime a p) : a ^ (p - 1) ≡ 1 [ZMOD p] := Int.ModEq.pow_card_sub_one_eq_one hp ha
euler_totienttheoremApplies a library theorempropext, Classical.choice, Quot.sound
euler_totientLean 4Applies a library theoremFormally verified
/-- **Euler's theorem:** if `gcd(a, n) = 1` then `a^φ(n) ≡ 1 (mod n)`. Mathlib's`Nat.ModEq.pow_totient`, proved there by Lagrange's theorem in the group of units of `ZMod n`. -/theorem euler_totient {a n : ℕ} (h : Nat.Coprime a n) : a ^ Nat.totient n ≡ 1 [MOD n] := Nat.ModEq.pow_totient h
wilsontheoremApplies a library theorempropext, Classical.choice, Quot.sound
wilsonLean 4Applies a library theoremFormally verified
/-- **Wilson's theorem:** `(p - 1)! ≡ -1 (mod p)` for every prime `p`. Mathlib's`ZMod.wilsons_lemma`, proved by pairing each residue with its inverse. -/theorem wilson (p : ℕ) [Fact p.Prime] : ((p - 1).factorial : ZMod p) = -1 := ZMod.wilsons_lemma p
carmichael_561theoremProved here from basic factspropext
carmichael_561Lean 4Proved here from basic factsFormally verified
/-- **The converse of Fermat fails.** `561 = 3 · 11 · 17` is not prime, yet `2⁵⁶⁰ ≡ 1 (mod 561)`:561 passes Fermat's test to base 2 (in fact to every base coprime to it — it is the smallestCarmichael number). `norm_num` certifies compositeness; `decide` checks the power. -/theorem carmichael_561 : ¬ Nat.Prime 561 ∧ 2 ^ 560 ≡ 1 [MOD 561] := by refine ⟨by norm_num, ?_⟩ decide +kernel
/-- Congruences can be multiplied.Hint: rewrite with `modEq_iff_dvd_sub`, use `a * c - b * d = a * (c - d) + d * (a - b)`(proved by `ring`), then `dvd_add` and `dvd_mul_of_dvd_right`. -/theorem modEq_mul {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] := by sorry
Show the compiled solution
modEq_mulLean 4Proved here from basic factsFormally verified
/-- **Congruences can be multiplied.** If `a ≡ b` and `c ≡ d (mod n)` then `ac ≡ bd`, because`ac - bd = a(c - d) + d(a - b)` and `n` divides both terms. -/theorem modEq_mul {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] := by rw [modEq_iff_dvd_sub] at h₁ h₂ ⊢ have h : a * c - b * d = a * (c - d) + d * (a - b) := by ring rw [h] exact dvd_add (dvd_mul_of_dvd_right h₂ a) (dvd_mul_of_dvd_right h₁ d)
/-- Uniqueness in the Chinese remainder theorem.Hint: `IsCoprime.mul_dvd` combines `m ∣ x - y` and `n ∣ x - y`. -/theorem crt_unique {m n x y : ℤ} (h : IsCoprime m n) (hm : x ≡ y [ZMOD m]) (hn : x ≡ y [ZMOD n]) : x ≡ y [ZMOD m * n] := by sorry
Show the compiled solution
crt_uniqueLean 4Proved here from basic factsFormally verified
/-- **Chinese remainder theorem, uniqueness.** If `m, n` are coprime and `x ≡ y` modulo both`m` and `n`, then `x ≡ y (mod mn)`: `m` and `n` both divide `x - y`, and coprime divisorsmultiply (Mathlib's `IsCoprime.mul_dvd`, itself proved from Bézout). -/theorem crt_unique {m n x y : ℤ} (h : IsCoprime m n) (hm : x ≡ y [ZMOD m]) (hn : x ≡ y [ZMOD n]) : x ≡ y [ZMOD m * n] := modEq_iff_dvd_sub.mpr (h.mul_dvd (modEq_iff_dvd_sub.mp hm) (modEq_iff_dvd_sub.mp hn))