2024-10-01から1ヶ月間の記事一覧
Mathematics In Leanから第7章 階層 7.1 基礎の勉強を続けます。 "At this stage we would like to move on to define rings"というあたりで、ここから環を定義していきます。 環を定義するにあたっての課題意識は環の2つの演算である加法群と乗法モノイド…
群にあってモノイドにないものは、、、そう、逆元です。モノイドにはすでに演算があり単位元があり演算は結合的でした。そこに全ての元に逆元があれば群になるわけです。 一旦前回までに定義した道具立てを再掲しておきます。 class Semigroup₂ (α : Type) e…
Mathematics In Leanから第7章 階層 7.1 基礎を勉強中です。 ここでは代数構造の階層を構成する方法を知ります。目的はその仕組みの概要を知ることで階層を使えるようになることだそうです。なので完全な理解というよりも主要な言葉や考え方などが理解できれ…