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
数学系のためのLean勉強会の「Advanced/Algebra」を見るのも良い
yuma-mizuno/lean-math-workshop: 数学系のためのLean勉強会
えびさんによる群の定義と証明
Leanにおける簡単な群の定義と、整数と加法が群の公理を満たすことの証明
https://www.youtube.com/watch?v=c1QZ8mUTjEo
群の定義
Lean 型クラス
関連
随伴
関手
帰納的型
商型
自由群
#Lean_4
#Lean_mathlib
#Lean