まとめ

代数の章で重要なのは，「構造」と「その構造を保つ写像」を型として読むことです． Group G，Ring R，Module R M のような型クラスが演算や公理を供給し， G →* H，R →+* S，Subgroup G，Ideal R のような bundled structure が数学的対象を表します．

証明では，手で公理を展開する前に，simp，group，abel，ring，rw，ext，#check を使って既存の構造を利用します．

形式化の tips

代数の形式化では，次の順に考えると進めやすくなります．

1. 対象は型か，部分構造か，準同型かを決める．
2. 演算が使えないときは，必要な型クラス仮定を探す．
3. 部分構造の等式は ext x で元ごとの同値にする．
4. membership は simp，rfl，Subgroup.mem_map などで開く．
5. 群や環の計算は group，abel，ring に任せる．