Maxima で綴る数学の旅

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