dvd_linear_combinationtheoremProved here from basic factspropext
dvd_linear_combinationLean 4Proved here from basic factsFormally verified
/-- If `d ∣ a` and `d ∣ b`, then `d` divides every integer combination `a·x + b·y`:from `a = d·k` and `b = d·l` we get `a·x + b·y = d·(k·x + l·y)`. -/theorem dvd_linear_combination {d a b : ℤ} (ha : d ∣ a) (hb : d ∣ b) (x y : ℤ) : d ∣ a * x + b * y := by obtain ⟨k, rfl⟩ := ha obtain ⟨l, rfl⟩ := hb exact ⟨k * x + l * y, by ring⟩
division_algorithmtheoremApplies a library theorempropext
division_algorithmLean 4Applies a library theoremFormally verified
/-- **Division with remainder** (existence): for `b > 0`, every integer `a` is `b·q + r` with`0 ≤ r < b`. This assembles core Lean's `Int.mul_ediv_add_emod`, `Int.emod_nonneg` and`Int.emod_lt_of_pos`, with `q = a / b` and `r = a % b`. -/theorem division_algorithm (a b : ℤ) (hb : 0 < b) : ∃ q r : ℤ, a = b * q + r ∧ 0 ≤ r ∧ r < b := ⟨a / b, a % b, (Int.mul_ediv_add_emod a b).symm, Int.emod_nonneg a hb.ne', Int.emod_lt_of_pos a hb⟩
division_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
division_uniqueLean 4Proved here from basic factsFormally verified
/-- **Division with remainder** (uniqueness): if `b·q + r = b·q' + r'` with both remainders in`[0, b)`, then `q = q'` and `r = r'`. Indeed `b·(q − q') = r' − r` lies strictly between `−b` and`b`, and the only multiple of `b` there is `0`. -/theorem division_unique {b q r q' r' : ℤ} (hb : 0 < b) (h : b * q + r = b * q' + r') (hr : 0 ≤ r) (hrb : r < b) (hr' : 0 ≤ r') (hrb' : r' < b) : q = q' ∧ r = r' := by have hq : q = q' := by by_contra hne rcases lt_or_gt_of_ne hne with hlt | hgt · have : b * q + b ≤ b * q' := by nlinarith linarith · have : b * q' + b ≤ b * q := by nlinarith linarith subst hq exact ⟨rfl, by linarith⟩
common_divisors_modtheoremProved here from basic factspropext
common_divisors_modLean 4Proved here from basic factsFormally verified
/-- **The key step of Euclid's algorithm**: `a, b` and `b, a mod b` have exactly the same commondivisors, because `a = b·(a / b) + (a mod b)`. -/theorem common_divisors_mod (a b d : ℕ) : (d ∣ a ∧ d ∣ b) ↔ (d ∣ b ∧ d ∣ a % b) := by have e : b * (a / b) + a % b = a := Nat.div_add_mod a b constructor · rintro ⟨ha, hb⟩ refine ⟨hb, ?_⟩ rw [← e] at ha exact (Nat.dvd_add_right (Dvd.dvd.mul_right hb _)).mp ha · rintro ⟨hb, hr⟩ refine ⟨?_, hb⟩ rw [← e] exact Nat.dvd_add (Dvd.dvd.mul_right hb _) hr
/-- **Euclid's algorithm**: `euclid a 0 = a`, and otherwise `euclid a b = euclid b (a mod b)`.It terminates because the second argument strictly decreases (`a mod b < b`), and a decreasingsequence of natural numbers cannot go on for ever. Lean checks this (`termination_by`). -/def euclid : ℕ → ℕ → ℕ | a, 0 => a | a, b + 1 => euclid (b + 1) (a % (b + 1))termination_by _ b => bdecreasing_by exact Nat.mod_lt _ (Nat.succ_pos _)
euclid_spectheoremProved here from basic factspropext, Quot.sound
euclid_specLean 4Proved here from basic factsFormally verified
/-- **Euclid's algorithm computes a greatest common divisor**: its output divides both inputs,and every common divisor of the inputs divides the output. Proof by induction following therecursion: when `b = 0` the output is `a`; otherwise apply `common_divisors_mod`. -/theorem euclid_spec (a b : ℕ) : (euclid a b ∣ a ∧ euclid a b ∣ b) ∧ ∀ d, d ∣ a → d ∣ b → d ∣ euclid a b := by induction a, b using euclid.induct with | case1 a => rw [euclid] exact ⟨⟨dvd_refl a, dvd_zero a⟩, fun d ha _ => ha⟩ | case2 a b ih => rw [euclid] obtain ⟨⟨h1, h2⟩, h3⟩ := ih refine ⟨(common_divisors_mod a (b + 1) _).mpr ⟨h1, h2⟩, fun d ha hdb => ?_⟩ exact h3 d hdb ((common_divisors_mod a (b + 1) d).mp ⟨ha, hdb⟩).2
euclid_eq_gcdtheoremProved here from basic factspropext, Quot.sound
euclid_eq_gcdLean 4Proved here from basic factsFormally verified
/-- Our `euclid` agrees with Lean's `Nat.gcd`: two numbers that divide each other are equal. -/theorem euclid_eq_gcd (a b : ℕ) : euclid a b = Nat.gcd a b := by obtain ⟨⟨h1, h2⟩, h3⟩ := euclid_spec a b exact Nat.dvd_antisymm (Nat.dvd_gcd h1 h2) (h3 _ (Nat.gcd_dvd_left a b) (Nat.gcd_dvd_right a b))
bezouttheoremProved here from basic factspropext, Classical.choice, Quot.sound
bezoutLean 4Proved here from basic factsFormally verified
/-- **Bézout's identity**, with the coefficients produced by `xgcd`:`a·x + b·y = gcd(a, b)`. Proof by induction following the recursion, using the back-substitutiondescribed in `xgcd`. -/theorem bezout (a b : ℕ) : (a : ℤ) * (xgcd a b).1 + (b : ℤ) * (xgcd a b).2 = (Nat.gcd a b : ℤ) := by rw [← euclid_eq_gcd] induction a, b using xgcd.induct with | case1 a => rw [xgcd, euclid] simp | case2 a b ih => rw [xgcd, euclid] have hcast : ((a % (b + 1) : ℕ) : ℤ) + ((b + 1 : ℕ) : ℤ) * ((a / (b + 1) : ℕ) : ℤ) = (a : ℤ) := by exact_mod_cast Nat.mod_add_div a (b + 1) simp only linear_combination ih - (xgcd (b + 1) (a % (b + 1))).2 * hcast
bezout_librarytheoremApplies a library theorempropext, Quot.sound
bezout_libraryLean 4Applies a library theoremFormally verified
/-- Bézout's identity in Mathlib: `Nat.gcd_eq_gcd_ab`, with Mathlib's extended Euclidean algorithm`Nat.gcdA`, `Nat.gcdB`. -/theorem bezout_library (a b : ℕ) : (Nat.gcd a b : ℤ) = a * Nat.gcdA a b + b * Nat.gcdB a b := Nat.gcd_eq_gcd_ab a b
euclid_lemmatheoremProved here from basic factspropext, Classical.choice, Quot.sound
euclid_lemmaLean 4Proved here from basic factsFormally verified
/-- **Euclid's lemma**: if a prime `p` divides `a·b`, then `p ∣ a` or `p ∣ b`.If `p ∤ a` then `gcd(p, a) = 1` (the only positive divisors of `p` are `1` and `p`), so by Bézout`p·x + a·y = 1`. Multiplying by `b`: `b = p·(b·x) + (a·b)·y`, and `p` divides both terms. -/theorem euclid_lemma {p a b : ℕ} (hp : p.Prime) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b := by by_cases hpa : p ∣ a · exact Or.inl hpa · right have hcop : Nat.gcd p a = 1 := (Nat.Prime.coprime_iff_not_dvd hp).mpr hpa have hbez := bezout p a rw [hcop, Nat.cast_one] at hbez have hZ : (p : ℤ) ∣ (a : ℤ) * (b : ℤ) := by exact_mod_cast h have key : (b : ℤ) = (p : ℤ) * ((b : ℤ) * (xgcd p a).1) + ((a : ℤ) * (b : ℤ)) * (xgcd p a).2 := by linear_combination (-(b : ℤ)) * hbez have : (p : ℤ) ∣ (b : ℤ) := by rw [key] exact dvd_add (dvd_mul_right _ _) (Dvd.dvd.mul_right hZ _) exact_mod_cast this
euclid_lemma_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
euclid_lemma_libraryLean 4Applies a library theoremFormally verified
/-- Euclid's lemma in Mathlib: `Nat.Prime.dvd_mul`. -/theorem euclid_lemma_library {p a b : ℕ} (hp : p.Prime) : p ∣ a * b ↔ p ∣ a ∨ p ∣ b := hp.dvd_mul
exists_prime_factorizationtheoremProved here from basic factspropext, Classical.choice, Quot.sound
exists_prime_factorizationLean 4Proved here from basic factsFormally verified
/-- **Existence of prime factorisations**, by strong induction: every `n ≥ 1` is the product of alist of primes (`1` is the empty product). For `n > 1`, let `p` be its smallest factor biggerthan `1` — a prime — and factorise the smaller number `n / p`. -/theorem exists_prime_factorization (n : ℕ) (hn : n ≠ 0) : ∃ l : List ℕ, (∀ p ∈ l, p.Prime) ∧ l.prod = n := by induction n using Nat.strong_induction_on with | _ n ih => by_cases h1 : n = 1 · exact ⟨[], by simp, by simp [h1]⟩ · have hp : (Nat.minFac n).Prime := Nat.minFac_prime h1 have hdiv : Nat.minFac n * (n / Nat.minFac n) = n := Nat.mul_div_cancel' (Nat.minFac_dvd n) have hlt : n / Nat.minFac n < n := Nat.div_lt_self (Nat.pos_of_ne_zero hn) hp.one_lt have hne : n / Nat.minFac n ≠ 0 := by intro h0 rw [h0, Nat.mul_zero] at hdiv exact hn hdiv.symm obtain ⟨l, hl, hprod⟩ := ih (n / Nat.minFac n) hlt hne refine ⟨Nat.minFac n :: l, ?_, ?_⟩ · intro q hq rcases List.mem_cons.mp hq with rfl | hq · exact hp · exact hl q hq · rw [List.prod_cons, hprod, hdiv]
prime_dvd_prodtheoremProved here from basic factspropext, Classical.choice, Quot.sound
prime_dvd_prodLean 4Proved here from basic factsFormally verified
/-- Euclid's lemma for several factors: if a prime divides a product of a list of numbers, itdivides one of them. Induction on the list, using `euclid_lemma` at each step. -/theorem prime_dvd_prod {p : ℕ} (hp : p.Prime) : ∀ l : List ℕ, p ∣ l.prod → ∃ q ∈ l, p ∣ q | [], h => absurd (Nat.dvd_one.mp h) hp.one_lt.ne' | q :: t, h => by rw [List.prod_cons] at h rcases euclid_lemma hp h with hq | ht · exact ⟨q, List.mem_cons_self, hq⟩ · obtain ⟨r, hr, hpr⟩ := prime_dvd_prod hp t ht exact ⟨r, List.mem_cons_of_mem q hr, hpr⟩
factorization_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
factorization_uniqueLean 4Proved here from basic factsFormally verified
/-- **Uniqueness of prime factorisations**: two lists of primes with the same product arerearrangements of each other (`List.Perm`, written `~`). Induction on the first list: its head `p`divides the product of the second, so (Euclid's lemma) it divides — hence equals — one of itsprimes `q`; remove `p` from both sides and cancel. -/theorem factorization_unique : ∀ l₁ l₂ : List ℕ, (∀ p ∈ l₁, p.Prime) → (∀ p ∈ l₂, p.Prime) → l₁.prod = l₂.prod → l₁.Perm l₂ | [], l₂, _, h₂, h => by cases l₂ with | nil => exact List.Perm.refl [] | cons q t => exfalso have hq : q ∣ (q :: t).prod := by rw [List.prod_cons]; exact dvd_mul_right q _ rw [← h, List.prod_nil] at hq exact (h₂ q List.mem_cons_self).one_lt.ne' (Nat.dvd_one.mp hq) | p :: t, l₂, h₁, h₂, h => by have hp : p.Prime := h₁ p List.mem_cons_self have hdvd : p ∣ l₂.prod := by rw [← h, List.prod_cons]; exact dvd_mul_right p _ obtain ⟨q, hq, hpq⟩ := prime_dvd_prod hp l₂ hdvd have hpq' : p = q := (Nat.prime_dvd_prime_iff_eq hp (h₂ q hq)).mp hpq subst hpq' have hperm : l₂.Perm (p :: l₂.erase p) := List.perm_cons_erase hq have hprod : t.prod = (l₂.erase p).prod := by have e : p * t.prod = p * (l₂.erase p).prod := by rw [← List.prod_cons, h, hperm.prod_eq, List.prod_cons] exact Nat.eq_of_mul_eq_mul_left hp.pos e have ht : t.Perm (l₂.erase p) := factorization_unique t (l₂.erase p) (fun r hr => h₁ r (List.mem_cons_of_mem p hr)) (fun r hr => h₂ r (List.mem_of_mem_erase hr)) hprod exact (ht.cons p).trans hperm.symm
factorization_unique_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
factorization_unique_libraryLean 4Applies a library theoremFormally verified
/-- Unique factorisation in Mathlib: `Nat.primeFactorsList_unique` — any list of primes withproduct `n` is a rearrangement of Mathlib's list `n.primeFactorsList`. -/theorem factorization_unique_library {n : ℕ} {l : List ℕ} (h₁ : l.prod = n) (h₂ : ∀ p ∈ l, p.Prime) : l.Perm n.primeFactorsList := Nat.primeFactorsList_unique h₁ h₂
prime_dvd_powtheoremProved here from basic factspropext, Classical.choice, Quot.sound
prime_dvd_powLean 4Proved here from basic factsFormally verified
/-- If a prime divides a power `n ^ k`, it divides `n`: Euclid's lemma applied `k` times(induction on `k`; for `k = 0`, no prime divides `1`). -/theorem prime_dvd_pow {p n : ℕ} (hp : p.Prime) : ∀ k : ℕ, p ∣ n ^ k → p ∣ n | 0, h => absurd (Nat.dvd_one.mp (by simpa using h)) hp.one_lt.ne' | k + 1, h => by rw [pow_succ] at h rcases euclid_lemma hp h with h1 | h2 · exact prime_dvd_pow hp k h1 · exact h2
terminating_prime_factorstheoremProved here from basic factspropext, Classical.choice, Quot.sound
terminating_prime_factorsLean 4Proved here from basic factsFormally verified
/-- **Terminating decimals, one direction.** A fraction `a / b` has a terminating decimal exactlywhen `a · 10ᵏ / b` is a whole number for some `k`, i.e. `b ∣ a · 10ᵏ`. If moreover `a / b` is inlowest terms (`gcd(a, b) = 1`), then every prime factor `p` of `b` is `2` or `5`: `p` divides`a · 10ᵏ` but not `a`, so (Euclid's lemma) it divides `10ᵏ`, hence `10 = 2 · 5`, hence `2` or `5`. -/theorem terminating_prime_factors {a b k p : ℕ} (hcop : Nat.gcd a b = 1) (h : b ∣ a * 10 ^ k) (hp : p.Prime) (hpb : p ∣ b) : p = 2 ∨ p = 5 := by have hpa10 : p ∣ a * 10 ^ k := Nat.dvd_trans hpb h rcases euclid_lemma hp hpa10 with hpa | hp10 · have : p ∣ Nat.gcd a b := Nat.dvd_gcd hpa hpb rw [hcop] at this exact absurd (Nat.dvd_one.mp this) hp.one_lt.ne' · have h10 : p ∣ 2 * 5 := prime_dvd_pow hp k hp10 rcases euclid_lemma hp h10 with h2 | h5 · exact Or.inl ((Nat.prime_dvd_prime_iff_eq hp Nat.prime_two).mp h2) · exact Or.inr ((Nat.prime_dvd_prime_iff_eq hp Nat.prime_five).mp h5)
two_five_dvd_ten_powtheoremProved here from basic factspropext
two_five_dvd_ten_powLean 4Proved here from basic factsFormally verified
/-- **Terminating decimals, the other direction.** If `b = 2ˢ · 5ᵗ`, then `b ∣ 10^(s + t)`, so`a / b = a · c / 10^(s + t)` for a whole number `c`: the decimal terminates after `s + t` digits(in fact after `max(s, t)`). Proof: `10^(s+t) = 2^(s+t) · 5^(s+t)`. -/theorem two_five_dvd_ten_pow (s t : ℕ) : 2 ^ s * 5 ^ t ∣ 10 ^ (s + t) := by have e : (10 : ℕ) ^ (s + t) = 2 ^ (s + t) * 5 ^ (s + t) := by rw [← mul_pow] rfl rw [e] exact Nat.mul_dvd_mul (Nat.pow_dvd_pow 2 (Nat.le_add_right s t)) (Nat.pow_dvd_pow 5 (Nat.le_add_left t s))
/-- In the **Hilbert numbers** `1, 5, 9, 13, …` (those leaving remainder `1` on division by `4`,which are closed under multiplication), `n > 1` is *irreducible* if it is not a product of twosmaller Hilbert numbers bigger than `1`. -/def HilbertIrreducible (n : ℕ) : Prop := n % 4 = 1 ∧ 1 < n ∧ ∀ a b : ℕ, (a % 4 = 1 ∧ b % 4 = 1 ∧ a * b = n) → a = 1 ∨ b = 1
hilbertIrreducible_ifftheoremProved here from basic factspropext, Quot.sound
hilbertIrreducible_iffLean 4Proved here from basic factsFormally verified
/-- Irreducibility is a **finite check**: if `a · b = n` with `n > 0`, both factors are at most `n`,so only `a, b ≤ n` need to be tried. -/theorem hilbertIrreducible_iff (n : ℕ) : HilbertIrreducible n ↔ n % 4 = 1 ∧ 1 < n ∧ ∀ a < n + 1, ∀ b < n + 1, (a % 4 = 1 ∧ b % 4 = 1 ∧ a * b = n) → a = 1 ∨ b = 1 := by constructor · rintro ⟨h4, h1, h⟩ exact ⟨h4, h1, fun a _ b _ hab => h a b hab⟩ · rintro ⟨h4, h1, h⟩ refine ⟨h4, h1, fun a b hab => ?_⟩ have hn : 0 < n := by omega have ha : a ≤ n := Nat.le_of_dvd hn ⟨b, hab.2.2.symm⟩ have hb : b ≤ n := Nat.le_of_dvd hn ⟨a, by rw [Nat.mul_comm]; exact hab.2.2.symm⟩ exact h a (by omega) b (by omega) hab
/-- A common divisor of `a` and `b` divides every combination `a * x + b * y`.Hint: `obtain ⟨k, rfl⟩ := ha`, `obtain ⟨l, rfl⟩ := hb`, then give the witness `k * x + l * y`and finish with `ring`. -/theorem dvd_linear_combination {d a b : ℤ} (ha : d ∣ a) (hb : d ∣ b) (x y : ℤ) : d ∣ a * x + b * y := by sorry
Show the compiled solution
dvd_linear_combinationLean 4Proved here from basic factsFormally verified
/-- If `d ∣ a` and `d ∣ b`, then `d` divides every integer combination `a·x + b·y`:from `a = d·k` and `b = d·l` we get `a·x + b·y = d·(k·x + l·y)`. -/theorem dvd_linear_combination {d a b : ℤ} (ha : d ∣ a) (hb : d ∣ b) (x y : ℤ) : d ∣ a * x + b * y := by obtain ⟨k, rfl⟩ := ha obtain ⟨l, rfl⟩ := hb exact ⟨k * x + l * y, by ring⟩
/-- Euclid's lemma needs primality: `4` divides `2 * 2` but not `2`.Hint: this is a finite check — `decide` can do it. -/theorem four_counterexample : 4 ∣ 2 * 2 ∧ ¬ 4 ∣ 2 := by sorry
Show the compiled solution
four_counterexampleLean 4Proved here from basic factsFormally verified
/-- **Primality matters in Euclid's lemma**: `4 ∣ 2·2`, but `4 ∤ 2`. -/theorem four_counterexample : 4 ∣ 2 * 2 ∧ ¬ 4 ∣ 2 := by decide