jurupapa https://blog.hatena.ne.jp/jurupapa/ Maxima で綴る数学の旅 https://maxima.hatenablog.jp/ 数学 前回の記事では普通の証明としてEuclideanDomainには零因子がないことを示しました。こんな感じでした。 $a, b$を零因子、すなわち$a\ne 0, b\ne 0, a * b=0$とします。$a * b = 0$及び$r\; 0\; a$から$r\; (a*b)\; a$。これはmul_left_not_lt a bに矛盾します。これで無事に任意のEuclideanDomainには零因子がないこと、すなわち整域であることが証明できました。 まあいいんですけど、この証明を見て細かいことを言えば$r\; 0\; a$は自明でしょうか。そういうことをきちんと詰めるための道具が形式的証明… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2024%2F06%2F27%2F220341" title="-数学- Lean4のお勉強　EuclidDomainは整域だ！形式証明しよう！ - Maxima で綴る数学の旅" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://cdn-ak.f.st-hatena.com/images/fotolife/j/jurupapa/20240602/20240602102318.jpg Hatena Blog https://hatena.blog 2024-06-27 22:03:41 rich https://maxima.hatenablog.jp/entry/2024/06/27/220341 1.0 100%