.. _basics:

Basics
======

This chapter is designed to introduce you to the nuts and
bolts of mathematical reasoning in Lean: calculating,
applying lemmas and theorems,
and reasoning about generic structures.

.. include:: 02_Basics/01_Calculating.inc

.. include:: 02_Basics/02_Proving_Identities_in_Algebraic_Structures.inc

.. include:: 02_Basics/03_Using_Theorems_and_Lemmas.inc

.. include:: 02_Basics/04_More_on_Order_and_Divisibility.inc

.. include:: 02_Basics/05_Proving_Facts_about_Algebraic_Structures.inc