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 を使う.