Leanで群論をやる
『Mathematics in Lean』
の8. Groups and Ringsをやる?
8. Groups and Rings — Mathematics in Lean 0.1 documentation
GitHub:
leanprover-community/mathematics_in_lean: The user home repository for the Mathematics in Lean tutorial.
これを見るのも良さそう
Group Theory in Lean
mathlib4での群論の定義
Mathlib.Algebra.Group.Basic
参考
https://www.youtube.com/watch?v=c1QZ8mUTjEo
随伴
関手
帰納的型
商型
自由群
#Lean_4
#Lean_mathlib
#Lean