今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。前回の記事でラグランジュの定理「有限群の元の個数は部分群の源の個数で割り切れる」をLean4で形式証明しました。 maxima.hatenablog.jp 証明の肝はSubgroup.groupEquivQuotien…

今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。 8.1.3のハイライトはラグランジュの定理です。 ラグランジュの定理：有限群の部分群の位数はもとの群の位数の約数である。 |G|=[G:G'] |G'| 、あるいは同じことだが、|G|=|G/G'…

Mathematics In Lean 4の第8章 群と環 に進みます。今回は8.1.3 部分群を読んでみます。 あるタイプAの元の集合が群をなすことを示すにはGroup A、Aの元の集合の部分集合がAの演算で群をなす（部分群になる）ことを示すにはSubgroup Aと書きます。演算が加法…

Mathematics In Lean 4の第8章 群と環 に進みます。第8章ではこれらの代数構造について部分集合や代数構造間の写像をLean4で表現する方法を学びます。代数構造としてはより単純なモノイドも扱います。演算の言葉として加法や乗法が出てきますが、主に記号の…