Entries from 2017-05-31 to 1 day
俺整数が加法に対してアーベル群をなす事の証明を洗練させてみた。全体的に、reflで整数から自然数の組に展開させて、 congで自然数の法則を使って、 symで自然数の組から整数に戻す、ということをやっている。仮定(postulate)したのは ・自然数の結合法則 …
俺整数が加法に対してアーベル群をなす事の証明を洗練させてみた。全体的に、reflで整数から自然数の組に展開させて、 congで自然数の法則を使って、 symで自然数の組から整数に戻す、ということをやっている。仮定(postulate)したのは ・自然数の結合法則 …