2012-01-10から1日間の記事一覧
今回は,以前(http://d.hatena.ne.jp/ehito/20111120),num_WFを用いて証明した が有理数でないこと です. let lemma01=MESON[GCD_ZERO; GCD_COPRIME_EXISTS] `~(a=0) ==> ?x y z. a=x*z /\ b=y*z /\ coprime(x,y)`;; let lemma02=NUM_RING`~(x * z = 0) ==…
今回は,以前(http://d.hatena.ne.jp/ehito/20111120),num_WFを用いて証明した が有理数でないこと です. let lemma01=MESON[GCD_ZERO; GCD_COPRIME_EXISTS] `~(a=0) ==> ?x y z. a=x*z /\ b=y*z /\ coprime(x,y)`;; let lemma02=NUM_RING`~(x * z = 0) ==…