times_ninety_eighttheoremProved here from basic factspropext
times_ninety_eightLean 4Proved here from basic factsFormally verified
/-- `a × 98 = a × 100 − a × 2` for every whole number `a`: since `100 = 98 + 2`, thedistributive law gives `a × 100 = a × 98 + a × 2`, and taking away `a × 2` leaves `a × 98`.So `7 × 98 = 700 − 14 = 686`. -/theorem times_ninety_eight (a : Nat) : a * 98 = a * 100 - a * 2 := by have h : a * 100 = a * 98 + a * 2 := calc a * 100 = a * (98 + 2) := rfl _ = a * 98 + a * 2 := Nat.mul_add a 98 2 rw [h, Nat.add_sub_cancel]
distrib_librarytheoremApplies a library theoremNo axioms
distrib_libraryLean 4Applies a library theoremFormally verified
/-- The distributive law `a × (b + c) = a × b + a × c`. This applies core Lean'stheorem `Nat.mul_add`. -/theorem distrib_library (a b c : Nat) : a * (b + c) = a * b + a * c := Nat.mul_add a b c
zero_mul_from_definitiontheoremProved here from basic factsNo axioms
zero_mul_from_definitionLean 4Proved here from basic factsFormally verified
/-- `0 × a = 0`: any number of copies of `0` add up to `0`. Proved by induction on `a`, usingonly Lean's definition `n * (m + 1) = n * m + n`. -/theorem zero_mul_from_definition (a : Nat) : 0 * a = 0 := by induction a with | zero => rfl | succ n ih => rw [Nat.mul_succ, ih]
succ_mul_from_definitiontheoremProved here from basic factspropext, Quot.sound
succ_mul_from_definitionLean 4Proved here from basic factsFormally verified
/-- `(a + 1) × b = a × b + b`: making every one of the `b` copies one bigger adds `b` in all.Proved by induction on `b` from the definition of multiplication. -/theorem succ_mul_from_definition (a b : Nat) : (a + 1) * b = a * b + b := by induction b with | zero => rfl | succ n ih => calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) := Nat.mul_succ (a + 1) n _ = a * n + n + (a + 1) := by rw [ih] _ = (a * n + a) + (n + 1) := by omega _ = a * (n + 1) + (n + 1) := by rw [Nat.mul_succ]
mul_comm_from_definitiontheoremProved here from basic factspropext, Quot.sound
mul_comm_from_definitionLean 4Proved here from basic factsFormally verified
/-- The commutative law `a × b = b × a`, proved from the definition of multiplication asrepeated addition (by induction on `b`, with the two lemmas above). Lean's `a * b` means"`b` copies of `a`", the opposite reading from "`a` groups of `b`"; this theorem is exactly whythe choice does not matter. -/theorem mul_comm_from_definition (a b : Nat) : a * b = b * a := by induction b with | zero => rw [Nat.mul_zero, zero_mul_from_definition] | succ n ih => rw [Nat.mul_succ, ih, succ_mul_from_definition]
mul_comm_librarytheoremApplies a library theoremNo axioms
mul_comm_libraryLean 4Applies a library theoremFormally verified
/-- The commutative law again, this time by applying core Lean's theorem `Nat.mul_comm`. -/theorem mul_comm_library (a b : Nat) : a * b = b * a := Nat.mul_comm a b
area_modeltheoremProved here from basic factspropext
area_modelLean 4Proved here from basic factsFormally verified
/-- The area model: `(a + b) × (c + d)` is the sum of the four partial products. Split thefirst factor (distributive law on the right), then split each part again (on the left). -/theorem area_model (a b c d : Nat) : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) := Nat.add_mul a b (c + d) _ = (a * c + a * d) + (b * c + b * d) := by rw [Nat.mul_add a c d, Nat.mul_add b c d] _ = a * c + a * d + b * c + b * d := (Nat.add_assoc (a * c + a * d) (b * c) (b * d)).symm
div_mod_existstheoremProved here from basic factspropext, Quot.sound
div_mod_existsLean 4Proved here from basic factsFormally verified
/-- Division with remainder always works: for `b > 0`, every `a` can be written as`a = q × b + r` with `r < b`. The proof adds eggs one at a time (induction on `a`). Each newegg either goes into the unfinished tray, or it completes that tray and the leftover pilestarts again at `0`. -/theorem div_mod_exists (a b : Nat) (hb : 0 < b) : ∃ q r, a = q * b + r ∧ r < b := by induction a with | zero => exact ⟨0, 0, by rw [Nat.zero_mul], hb⟩ | succ n ih => obtain ⟨q, r, h, _hr⟩ := ih by_cases hfit : r + 1 < b · -- The new egg fits in the unfinished tray: the remainder grows by one. exact ⟨q, r + 1, by omega, hfit⟩ · -- The new egg completes the tray (`r + 1 = b`): one more full tray, nothing left over. have hrb : r + 1 = b := by omega refine ⟨q + 1, 0, ?_, hb⟩ calc n + 1 = q * b + (r + 1) := by omega _ = q * b + b := by rw [hrb] _ = (q + 1) * b + 0 := by rw [Nat.succ_mul, Nat.add_zero]
div_mod_uniquetheoremProved here from basic factspropext, Quot.sound
div_mod_uniqueLean 4Proved here from basic factsFormally verified
/-- The quotient and remainder are unique. If `q × b + r = q' × b + r'` with both remaindersless than `b`, then `q = q'` and `r = r'`. If `q` were smaller than `q'`, the right sidewould be at least `(q + 1) × b = q × b + b`, which is more than `q × b + r`. -/theorem div_mod_unique {b q r q' r' : Nat} (h : q * b + r = q' * b + r') (hr : r < b) (hr' : r' < b) : q = q' ∧ r = r' := by have hq : q = q' := by rcases Nat.lt_trichotomy q q' with hlt | heq | hgt · have hle : (q + 1) * b ≤ q' * b := Nat.mul_le_mul_right b hlt rw [Nat.succ_mul] at hle omega · exact heq · have hle : (q' + 1) * b ≤ q * b := Nat.mul_le_mul_right b hgt rw [Nat.succ_mul] at hle omega subst hq exact ⟨rfl, by omega⟩
div_mod_librarytheoremApplies a library theorempropext
div_mod_libraryLean 4Applies a library theoremFormally verified
/-- Lean's own quotient `a / b` and remainder `a % b` satisfy `a = (a / b) × b + a % b` with`a % b < b`. This applies the core theorems `Nat.div_add_mod'` and `Nat.mod_lt`. -/theorem div_mod_library (a b : Nat) (hb : 0 < b) : a = a / b * b + a % b ∧ a % b < b := ⟨(Nat.div_add_mod' a b).symm, Nat.mod_lt a hb⟩
no_division_by_zerotheoremProved here from basic factsNo axioms
no_division_by_zeroLean 4Proved here from basic factsFormally verified
/-- There is no answer to `5 ÷ 0`: no number `q` has `q × 0 = 5`, because `q × 0 = 0`. -/theorem no_division_by_zero : ¬ ∃ q : Nat, q * 0 = 5 := by intro ⟨q, hq⟩ rw [Nat.mul_zero] at hq -- `hq : 0 = 5`, which is false. exact absurd hq (by decide)
multiplying_need_not_enlargetheoremProved here from basic factsNo axioms
multiplying_need_not_enlargeLean 4Proved here from basic factsFormally verified
/-- "Multiplying always makes a number bigger" is false. One counterexample is enough:`9 × 1 = 9` is not bigger than `9`. -/theorem multiplying_need_not_enlarge : ¬ ∀ a b : Nat, a < a * b := by intro h have h91 : 9 < 9 * 1 := h 9 1 exact absurd h91 (by decide)
/-- Prove the area model: `(a + b) × (c + d)` is the sum of four partial products.Hint: `Nat.add_mul` splits the first factor, `Nat.mul_add` splits the second,and `Nat.add_assoc` regroups the sum. -/theorem area_model (a b c d : Nat) : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by sorry
Show the compiled solution
area_modelLean 4Proved here from basic factsFormally verified
/-- The area model: `(a + b) × (c + d)` is the sum of the four partial products. Split thefirst factor (distributive law on the right), then split each part again (on the left). -/theorem area_model (a b c d : Nat) : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) := Nat.add_mul a b (c + d) _ = (a * c + a * d) + (b * c + b * d) := by rw [Nat.mul_add a c d, Nat.mul_add b c d] _ = a * c + a * d + b * c + b * d := (Nat.add_assoc (a * c + a * d) (b * c) (b * d)).symm
/-- Show that no number `q` satisfies `q × 0 = 5`.Hint: after `intro ⟨q, hq⟩`, rewrite `hq` with `Nat.mul_zero`. -/theorem no_division_by_zero : ¬ ∃ q : Nat, q * 0 = 5 := by sorry
Show the compiled solution
no_division_by_zeroLean 4Proved here from basic factsFormally verified
/-- There is no answer to `5 ÷ 0`: no number `q` has `q × 0 = 5`, because `q × 0 = 0`. -/theorem no_division_by_zero : ¬ ∃ q : Nat, q * 0 = 5 := by intro ⟨q, hq⟩ rw [Nat.mul_zero] at hq -- `hq : 0 = 5`, which is false. exact absurd hq (by decide)