Chapter 01: 代数

Mathlib における代数構造の扱いを概観します．

参考:

• Mathematics in Lean, 9. Groups and Rings: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

中心になる考え方は次の 3 つです．

• 代数構造は型クラスで表す．
• 準同型や部分構造は bundled structure として表す．
• 具体的な計算には simp，group，abel，ring などの tactic を使う．

import Mathlib

namespace PracticeChapter01