Lumenary.Modular

Formal library

• clock_wrapstheoremProved here from basic factsNo axioms

  /-- On a 12-hour clock, 5 hours after 9 o'clock is 2 o'clock: `(9 + 5) mod 12 = 2`. -/
  theorem clock_wraps : (9 + 5) % 12 = 2 := by decide

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor

• three_inv_mod_seventheoremProved here from basic factsNo axioms

  /-- Modulo 7, the number 3 has an inverse, namely 5: `3 · 5 = 15 = 2 · 7 + 1`. -/
  theorem three_inv_mod_seven : (3 * 5) % 7 = 1 := by decide

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor

• two_no_inv_mod_fourtheoremProved here from basic factsNo axioms

  /-- Modulo 4, the number 2 has **no** inverse: `2 · x` is always even, so it is never `1`
  more than a multiple of 4. `decide` checks all four possibilities `x = 0, 1, 2, 3`. -/
  theorem two_no_inv_mod_four : ∀ x : Fin 4, (2 * x.val) % 4 ≠ 1 := by decide

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor

• inverses_mod_fivetheoremProved here from basic factspropext, Quot.sound

  /-- Modulo 5 (a prime), every non-zero number has an inverse:
  `1·1 = 1`, `2·3 = 6`, `3·2 = 6`, `4·4 = 16`, and each of these leaves remainder 1.
  `decide` checks every `a` and searches for each `b`. -/
  theorem inverses_mod_five : ∀ a : Fin 5, a.val ≠ 0 → ∃ b : Fin 5, (a.val * b.val) % 5 = 1 := by
    decide

  Axioms used: propext, Quot.soundformal/Lumenary/Modular.leanTry it in the Lean web editor

• mod_add_modtheoremApplies a library theorempropext

  /-- You may reduce before or after adding: `(a mod k + b mod k) mod k = (a + b) mod k`.
  This applies core Lean's `Nat.add_mod`. -/
  theorem mod_add_mod (a b k : Nat) : (a % k + b % k) % k = (a + b) % k :=
    (Nat.add_mod a b k).symm

  Axioms used: propextformal/Lumenary/Modular.leanTry it in the Lean web editor

• ModEqdefDefinitionNo axioms

  /-- `ModEq k a b` ("`a ≡ b (mod k)`"): `a` and `b` leave the same remainder on division by `k`.
  (Mathlib analogue: `Int.ModEq`, defined the same way.) -/
  def ModEq (k a b : Int) : Prop := a % k = b % k

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor

• modEq_refltheoremProved here from basic factsNo axioms

  /-- Every integer is congruent to itself. -/
  theorem modEq_refl (k a : Int) : ModEq k a a := rfl

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor

• modEq_symmtheoremProved here from basic factsNo axioms

  /-- If `a ≡ b` then `b ≡ a`. -/
  theorem modEq_symm {k a b : Int} (h : ModEq k a b) : ModEq k b a := Eq.symm h

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor

• modEq_transtheoremProved here from basic factsNo axioms

  /-- If `a ≡ b` and `b ≡ c` then `a ≡ c`: equal remainders chain together. -/
  theorem modEq_trans {k a b c : Int} (h₁ : ModEq k a b) (h₂ : ModEq k b c) : ModEq k a c :=
    Eq.trans h₁ h₂

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor

• modEq_equivalencetheoremProved here from basic factsNo axioms

  /-- Congruence modulo `k` is an **equivalence relation** (reflexive, symmetric, transitive).
  Its equivalence classes are the "hours" on a `k`-hour clock. -/
  theorem modEq_equivalence (k : Int) : Equivalence (ModEq k) :=
    ⟨modEq_refl k, modEq_symm, modEq_trans⟩

  Axioms used: No axiomsformal/Lumenary/Modular.leanTry it in the Lean web editor