2016-10-10から1日間の記事一覧
理解したい。問題は、OCaml読めないことと、HOL Lightが、どういうものか微塵も分からんので、とりあえず、HOL Lightを動かしてみたメモ。ソースコード落とすと、中にTutorialがあるので適当に見れば良い気がする。 Coqと双璧をなすかどうかは知らないけど、…
前回の補足など。 前回、極小表現上で消えるU(so(4,2))の元全体をJosephイデアルと呼んでしまったけど、Josephイデアルの(数学者が一般的に採用する)定義は、複素単純Lie代数の普遍展開環のcompletely prime primitive idealであって、so(4,2)は複素単純では…