2016-10-10から1日間の記事一覧

HOL Lightの実装を理解したい(0)

理解したい。問題は、OCaml読めないことと、HOL Lightが、どういうものか微塵も分からんので、とりあえず、HOL Lightを動かしてみたメモ。ソースコード落とすと、中にTutorialがあるので適当に見れば良い気がする。 Coqと双璧をなすかどうかは知らないけど、…

水素原子の表現論(1.5-2)spectrum generating algebra

前回の補足など。 前回、極小表現上で消えるU(so(4,2))の元全体をJosephイデアルと呼んでしまったけど、Josephイデアルの(数学者が一般的に採用する)定義は、複素単純Lie代数の普遍展開環のcompletely prime primitive idealであって、so(4,2)は複素単純では…