Natural numbers

inductive MyNat : Type

• zero : MyNat
• succ : MyNat → MyNat

Addition

Here we define addition of natural numbers.

def MyNat.add (a b : MyNat) : MyNat

Natural number addition.

Equations

• a.add MyNat.zero = a
• a.add b_2.succ = (a.add b_2).succ

@[simp]

theorem MyNat.zero_add (a : MyNat) : zero.add a = a

For any natural number $a$, $0 + a = a$, where $+$ is Def. MyNat.add.

theorem MyNat.succ_add (a b : MyNat) : a.succ.add b = (a.add b).succ

For any natural numbers $a, b$, $(a + 1) + b = (a + b) + 1$.

theorem MyNat.add_comm (a b : MyNat) : a.add b = b.add a

For any natural numbers $a, b$, $a + b = b + a$.

Multiplication

def MyNat.mul (a b : MyNat) : MyNat

Natural number multiplication.

Equations

• a.mul b = sorry

theorem MyNat.mul_comm (a b : MyNat) : a.mul b = b.mul a

For any natural numbers $a, b$, $a * b = b * a$.

Fermat's Last Theorem

theorem MyNat.flt : sorry

Fermat's last theorem.

In the docstring, usual Markdown features and math mode are supported (by MD4Lean), with additional support for citations like [Wiles1995] using [square brackets] and references to other nodes like MyNat.zero_add using inline `code`.

You can also directly input raw LaTeX, e.g. as follows:

\begin{thebibliography}{9}

\bibitem{Wiles1995} Andrew Wiles (1995) \emph{Modular elliptic curves and Fermat's last theorem}, Annals of Mathematics, 141(3), 443--551.

\bibitem{Taylor-Wiles1995} Richard Taylor and Andrew Wiles (1995) \emph{Ring-theoretic properties of certain Hecke algebras}, Annals of Mathematics, 141(3), 553--572.

\end{thebibliography}