Provede2eimport-fixture

triple n + 0 = n + n + n

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{triple}}(\htmlData{mx=1}{n})} + 0} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{\htmlData{mx=6}{\htmlData{mx=4}{n} + \htmlData{mx=5}{n}} + \htmlData{mx=7}{n}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
triple: triple: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (triple)
f(x)Function application: triple applied to n. Lean writes f x; papers write f(x). (triple n)
+Addition: triple(n) plus 0. (triple n + 0)
=Equality: triple(n) + 0 and n + n + n are the same. (triple n + 0 = n + n + n)

theorem triple-unfold-zero-231159 (n : Nat) :
    triple n + 0 = n + n + n

How it was proved

Proved: 24 September 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: None
Proof: 0 lines of Lean