1. Addition
- No associated Lean code or declarations.
We write a + b for the result of adding b to a.
This starter Blueprint begins with the most basic sanity checks around that
operation.
-
nat_add_zero_right[complete]
For every natural number n, adding zero on the right leaves it unchanged:
n + 0 = n.
This is the first sanity check for Definition 1.1.
Induct on n. The base case is immediate and the inductive step unfolds one
successor on each side.
Lean code for Theorem1.2
Associated Lean declarations
-
nat_add_zero_right[complete]
-
nat_add_zero_right[complete]
theorem nat_add_zero_right (n : Nat) : n + 0 = n := n:Nat⊢ n + 0 = n
All goals completed! 🐙
-
Nat.add_assoc[complete]
For all natural numbers a, b, and c, addition is associative:
(a + b) + c = a + (b + c).
This is another consequence of Definition 1.1.
Lean code for Theorem1.3●1 theorem
Associated Lean declarations
-
Nat.add_assoc[complete]
-
Nat.add_assoc[complete]
-
theoremdefined in Init/Data/Nat/Basic.leancomplete
theorem Nat.add_assoc (n m k : Nat) : n + m + k = n + (m + k)
theorem Nat.add_assoc (n m k : Nat) : n + m + k = n + (m + k)
Lean already provides this theorem as Nat.add_assoc, so this Blueprint entry
links to an existing declaration instead of restating the code locally.
- No associated Lean code or declarations.
Some projects keep implementation notes or helper snippets next to the informal statement surface. Blueprint can attach a small Rust block for that purpose.
Rust code for Definition1.4
pub fn add_preview(x: i32, y: i32) -> i32 { x + y }