Mathematics In Leanから第7章 階層 7.1 基礎を勉強中です。 ここでは代数構造の階層を構成する方法を知ります。目的はその仕組みの概要を知ることで階層を使えるようになることだそうです。なので完全な理解というよりも主要な言葉や考え方などが理解できれば良いと思います。 実は夏前に7.1 基礎を読んだ時には何をやっているのかいまいちわからず、ちょっと困っていました。夏の暑い間はLean 4はお休みしていたのですが、最近勉強を復活しつつあります。まだ理解が足りていないところが多そうなのですが、まあそこは上記のように割り切って進めることにします。 具体的には7.1では半群、モノイド、…