Starter Blueprint

2. Multiplication🔗

Definition2.1
Group: Core statements about multiplication on natural numbers. (2)
Group member previews
Preview
Theorem 2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N

We write a * b for the product of a and b. One way to think about multiplication is as repeated addition, building on Definition 1.1.

Theorem2.2
Group: Core statements about multiplication on natural numbers. (2)
Group member previews
Preview
Definition 2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsstarterarithmetic

For every natural number n, multiplying by one on the right leaves it unchanged: n * 1 = n. This is the first sanity check for Definition 2.1.

Proof for Theorem 2.2
uses 0

Unfold the definition of multiplication and simplify.

Lean code for Theorem2.2theorem multiplication_one_right (n : Nat) : n * 1 = n := n:Nat⊢ n * 1 = n All goals completed! 🐙
Theorem2.3
Group: Core statements about multiplication on natural numbers. (2)
Group member previews
Preview
Definition 2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

For all natural numbers a, b, and c, multiplication is associative: (a * b) * c = a * (b * c).

Lean code for Theorem2.3●1 theorem
  • theoremdefined in Init/Data/Nat/Basic.lean
    complete
    theorem Nat.mul_assoc (n m k : Nat) : n * m * k = n * (m * k)
    theorem Nat.mul_assoc (n m k : Nat) :
  n * m * k = n * (m * k)
Proof for Theorem 2.3
uses 0

Lean already provides this theorem as Nat.mul_assoc, so this Blueprint entry links to an existing declaration instead of restating the code locally.