1. Core Previews
Definition1.1
Group: Core statements that drive the showcase summary and dependency graph. (3)
Lean status
- No associated Lean code or declarations.
Base statement for summary and graph previews.
Lemma1.2
Depends on Definition 1.1.
Definition1.3
Statement with an associated Lean declaration link in the summary.
Lean code for Definition1.3●1 definition
Associated Lean declarations
-
Nat.add[complete]
Associated Lean declarations
-
Nat.add[complete]
-
defdefined in Init/Prelude.leancomplete
def Nat.add : Nat → Nat → Nat
def Nat.add : Nat → Nat → Nat
Addition of natural numbers, typically used via the `+` operator. This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Theorem1.4
Group: Core statements that drive the showcase summary and dependency graph. (3)
Statement uses 2
Lean status
- No associated Lean code or declarations.
Combines Lemma 1.2 with Definition 1.3.