jurupapa https://blog.hatena.ne.jp/jurupapa/ Maxima で綴る数学の旅 https://maxima.hatenablog.jp/ 数学 Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。 最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです。$\sqrt{2}$が実数の中に存在することまで示すわけではありません。 証明は古代ギリシャから知られているものです。$\sqrt{2}=\frac{m}{n}$となる互いに素な自然数$m,n$が存在するとします。すると $$m^2=2\,n^2$$ です。ここから$m$が偶数であることがわかります。$m=2\… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2024%2F03%2F23%2F154822" title="-数学- Lean4のお勉強　$\sqrt{2}$が無理数であること - 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/20240323/20240323154718.jpg Hatena Blog https://hatena.blog 2024-03-23 15:48:22 rich https://maxima.hatenablog.jp/entry/2024/03/23/154822 1.0 100%