### Peano numbers in Lean

In this post, I will define the natural numbers using the Peano axioms and prove that the set of natural numbers $\N$ equipped with ordinary addition and multiplication is a commutative semiring.

In this post, I will define the natural numbers using the Peano axioms and prove that the set of natural numbers $\N$ equipped with ordinary addition and multiplication is a commutative semiring.

For the most part of the programming projects I am working, I like to specify some aliases for common terminal commands. Them problem is… I have never been satisfied on how to specify such aliases.