チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

2012-12-23から1日間の記事一覧

Coq でモジュラー束

この記事は LL/ML Advent Calendar の 23 日目です。「タイトルに "LL" もしくは "ML" を含むこと」という謎ルールに従い、「群の正規部分群の全体がモジュラー束 (Modular Lattices) をなすこと」を Coq により証明してみました。なお、完全なコードは http…