.. _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.

この章では，Leanにおける数学的推論の基本を紹介します．計算や補題・定理の適用，一般的な構造についての推論を扱います．

.. include:: C02_Basics/S01_Calculating.inc
.. include:: C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.inc
.. include:: C02_Basics/S03_Using_Theorems_and_Lemmas.inc
.. include:: C02_Basics/S04_More_on_Order_and_Divisibility.inc
.. include:: C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.inc