Leanで群論をやる
数学系のためのLean勉強会の「Advanced/Algebra」を見るのも良い
lean-math-workshop/Tutorial/Advanced/Algebra
『Mathematics in Lean』
の8. Groups and Ringsをやる？
9. Groups and Rings — Mathematics in Lean v4.19.0 documentation
これを見るのも良さそう
Mitchell Rowet.
Group Theory in Lean
mathlib4での群論の定義
Mathlib.Algebra.Group.Basic
えびさんによる群の定義と証明
Leanにおける簡単な群の定義と、整数と加法が群の公理を満たすことの証明
https://www.youtube.com/watch?v=c1QZ8mUTjEo
Lean 型クラス
関連
随伴
関手
帰納的型
商型
自由群
#Lean_4
#Mathlib
#Lean