div_add_modtheoremApplies a library theorempropext
div_add_modLean 4Applies a library theoremFormally verified
/-- **Division with remainder.** Every `a` is `n` times its quotient plus its remainder:`n · (a / n) + a % n = a`. This applies core Lean's `Nat.div_add_mod`. -/theorem div_add_mod (a n : Nat) : n * (a / n) + a % n = a := Nat.div_add_mod a n
mod_ltLean 4Applies a library theoremFormally verified
/-- A remainder on division by `n > 0` is always one of `0, 1, …, n - 1`: `a % n < n`.This applies core Lean's `Nat.mod_lt`. -/theorem mod_lt (a : Nat) {n : Nat} (hn : 0 < n) : a % n < n := Nat.mod_lt a hn
week_exampletheoremProved here from basic factsNo axioms
week_exampleLean 4Proved here from basic factsFormally verified
/-- Number the days Monday = 0, Tuesday = 1, …, Sunday = 6. Then 100 days after a Monday isday `100 mod 7 = 2`, a Wednesday. -/theorem week_example : (0 + 100) % 7 = 2 := by decide
add_mod_of_divisiontheoremProved here from basic factspropext, Quot.sound
add_mod_of_divisionLean 4Proved here from basic factsFormally verified
/-- **The remainder of a sum depends only on the remainders.**`(a + b) mod n = ((a mod n) + (b mod n)) mod n`.The lesson's proof: write `a = n·q₁ + r₁` and `b = n·q₂ + r₂`. Then`a + b = n·(q₁ + q₂) + (r₁ + r₂)`, and adding a multiple of `n` never changes a remainder(`Nat.mul_add_mod`). -/theorem add_mod_of_division (a b n : Nat) : (a + b) % n = (a % n + b % n) % n := by -- The two divisions with remainder. have ha := Nat.div_add_mod a n have hb := Nat.div_add_mod b n -- Regroup: `a + b` is a multiple of `n` plus `r₁ + r₂`. have hsum : a + b = n * (a / n + b / n) + (a % n + b % n) := by calc a + b = (n * (a / n) + a % n) + (n * (b / n) + b % n) := by rw [ha, hb] _ = n * (a / n + b / n) + (a % n + b % n) := by rw [Nat.mul_add]; omega rw [hsum, Nat.mul_add_mod]
mul_mod_of_divisiontheoremProved here from basic factspropext
mul_mod_of_divisionLean 4Proved here from basic factsFormally verified
/-- **The remainder of a product depends only on the remainders.**`(a · b) mod n = ((a mod n) · (b mod n)) mod n`.Proof: with `a = n·q₁ + r₁` and `b = n·q₂ + r₂`, expanding gives`a · b = n·(q₁·b + r₁·q₂) + r₁·r₂`, a multiple of `n` plus `r₁ · r₂`. -/theorem mul_mod_of_division (a b n : Nat) : (a * b) % n = (a % n * (b % n)) % n := by have ha := Nat.div_add_mod a n have hb := Nat.div_add_mod b n have hprod : a * b = n * (a / n * b + a % n * (b / n)) + a % n * (b % n) := by calc a * b = (n * (a / n) + a % n) * b := by rw [ha] _ = n * (a / n) * b + a % n * b := Nat.add_mul _ _ _ _ = n * (a / n) * b + a % n * (n * (b / n) + b % n) := by rw [hb] _ = n * (a / n * b + a % n * (b / n)) + a % n * (b % n) := by rw [Nat.mul_add (a % n), Nat.mul_add n, Nat.mul_assoc, ← Nat.add_assoc, Nat.mul_left_comm (a % n) n] rw [hprod, Nat.mul_add_mod]
add_mod_librarytheoremApplies a library theorempropext
add_mod_libraryLean 4Applies a library theoremFormally verified
/-- The same fact for sums, quoted from core Lean's library (`Nat.add_mod`). Compare`add_mod_of_division`, which proves it here from division with remainder. -/theorem add_mod_library (a b n : Nat) : (a + b) % n = (a % n + b % n) % n := Nat.add_mod a b n
no_partner_of_common_factortheoremProved here from basic factspropext, Quot.sound
no_partner_of_common_factorLean 4Proved here from basic factsFormally verified
/-- **A common factor blocks a partner.** If some `d > 1` divides both `a` and `n`, then no `b`has `a · b mod n = 1`.Proof: `d` divides `a · b`, and `d` divides `n`, so `d` divides the remainder `a · b mod n`(the remainder is `a · b` minus a multiple of `n`). If that remainder were `1`, then `d` woulddivide `1`, so `d = 1`, contradicting `d > 1`. -/theorem no_partner_of_common_factor {a n d : Nat} (hd : 1 < d) (hda : d ∣ a) (hdn : d ∣ n) (b : Nat) : (a * b) % n ≠ 1 := by intro h -- `d` divides `a · b` … have hab : d ∣ a * b := Nat.dvd_mul_right_of_dvd hda b -- … so it divides the remainder of `a · b` on division by `n`, which is `1`. have h1 : d ∣ (a * b) % n := (Nat.dvd_mod_iff hdn).mpr hab rw [h] at h1 have : d = 1 := Nat.eq_one_of_dvd_one h1 omega
partners_mod_twelvetheoremProved here from basic factspropext, Quot.sound
partners_mod_twelveLean 4Proved here from basic factsFormally verified
/-- On a 12-hour clock exactly `1, 5, 7, 11` have a multiplicative partner. Lean's `Fin 12`is clock arithmetic: its numbers are `0, …, 11` and `*` multiplies and takes the remainder.`decide` checks all 144 products. -/theorem partners_mod_twelve : ∀ a : Fin 12, (∃ b : Fin 12, a * b = 1) ↔ (a = 1 ∨ a = 5 ∨ a = 7 ∨ a = 11) := by decide
partners_mod_seventheoremProved here from basic factspropext, Quot.sound
partners_mod_sevenLean 4Proved here from basic factsFormally verified
/-- Modulo the prime `7`, every non-zero remainder has a partner(`1·1`, `2·4`, `3·5`, `6·6` all leave remainder `1`). `decide` checks every case. -/theorem partners_mod_seven : ∀ a : Fin 7, a ≠ 0 → ∃ b : Fin 7, a * b = 1 := by decide
row_is_shuffle_mod_seventheoremProved here from basic factspropext
row_is_shuffle_mod_sevenLean 4Proved here from basic factsFormally verified
/-- Modulo `7`, multiplying by a non-zero `a` never sends two different remainders to thesame place: each row of the multiplication table is a shuffle of `0, …, 6`. (This is theproperty check digits rely on.) -/theorem row_is_shuffle_mod_seven : ∀ a x y : Fin 7, a ≠ 0 → a * x = a * y → x = y := by decide
ten_pow_mod_ninetheoremProved here from basic factspropext
ten_pow_mod_nineLean 4Proved here from basic factsFormally verified
/-- `10^k mod 9 = 1` for every `k`, because `10 = 9 + 1` leaves remainder `1`. This is why anumber and the sum of its digits leave the same remainder on division by `9`("casting out nines"). -/theorem ten_pow_mod_nine (k : Nat) : 10 ^ k % 9 = 1 := by induction k with | zero => decide | succ k ih => calc 10 ^ (k + 1) % 9 = (10 ^ k * 10) % 9 := by rw [Nat.pow_succ] _ = (10 ^ k % 9 * (10 % 9)) % 9 := mul_mod_of_division _ _ _ _ = 1 := by rw [ih]
/-- Show that `4` has no multiplicative partner modulo `10`.Hint: `4` and `10` have the common factor `2`. Use`Lumenary.ModularArithmetic.no_partner_of_common_factor (d := 2)`; each of its three sideconditions can be closed `by decide`. -/theorem four_no_partner_mod_ten (b : Nat) : (4 * b) % 10 ≠ 1 := by sorry
Show the compiled solution
four_no_partner_mod_tenLean 4Proved here from basic factsFormally verified
/-- `4` has no partner modulo `10`: `4` and `10` share the factor `2`. This is`no_partner_of_common_factor` with `d = 2`. -/theorem four_no_partner_mod_ten (b : Nat) : (4 * b) % 10 ≠ 1 := no_partner_of_common_factor (d := 2) (by decide) (by decide) (by decide) b
/-- Casting out nines: show that `10^k` leaves remainder `1` on division by `9`.Hint: induction on `k`. In the step, rewrite `10^(k+1)` as `10^k * 10` (`Nat.pow_succ`), thenuse `Lumenary.ModularArithmetic.mul_mod_of_division` and the induction hypothesis. -/theorem ten_pow_mod_nine (k : Nat) : 10 ^ k % 9 = 1 := by sorry
Show the compiled solution
ten_pow_mod_nineLean 4Proved here from basic factsFormally verified
/-- `10^k mod 9 = 1` for every `k`, because `10 = 9 + 1` leaves remainder `1`. This is why anumber and the sum of its digits leave the same remainder on division by `9`("casting out nines"). -/theorem ten_pow_mod_nine (k : Nat) : 10 ^ k % 9 = 1 := by induction k with | zero => decide | succ k ih => calc 10 ^ (k + 1) % 9 = (10 ^ k * 10) % 9 := by rw [Nat.pow_succ] _ = (10 ^ k % 9 * (10 % 9)) % 9 := mul_mod_of_division _ _ _ _ = 1 := by rw [ih]