MIL

ちょっとだけ環論の基礎の復習です。 可換環とは加法と乗法が定義されており、それぞれの単位元が0, 1であり、どちらもどちらも可換、かつ分配法則が成り立つ集合です。 整域とは零因子のない可換環でかつ自明でない環です。 $a, b$が零因子とは$a\ne 0, b\ne 0, a\,b=0$となるような$a,b$のことでした。また環が自明とは$0=1$が成り立つことでした。 ユークリッド整域($R$)とは整域でかつ除法の原理を満たすノルムと呼ばれる関数$f:R\rightarrow \mathbb{N}$が定義されていることをいう。 除法の原理：$a=b\,q+r, f(r)\lt f(a)$。 …

Mathematics in Lean4の数論の章の３つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として３つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して必ずnよりも大きな素数が存在する（作れる）ことを示す。theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by... 素数が有限個しかないとして、それらの積に1を足した数を考えるとその素因数が元の素数の集合に含まれることから矛盾を導く（ユークリッド）。theorem primes…

Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつBがAの部分集合であることを示すこと AがBの部分集合であることを示すにはAの任意の要素がBの要素であることを示すこと 空集合と全体集合の性質 和集合と積集合をメンバーシップの論理和と論理積 集合族の積集合と和集合 のようなことがここでは解説されています。ここでは上記の初めの２つについて簡単な命題を示し…

"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b （a, bの小さい方を返す）について次の性質の証明です。 min a (min b c) = min (min a b) c 直感的には結局両辺ともa,b,cのうち最小の値を返しますから等しくなるのは納得です。一方この学習では以下の４つの性質だけから上記の性質を示すことが課題です。 le_antisymm : a $\le$ b $\land$ b $\le$ a $\iff$ a=b min_…