高校
三乗は、9の時計では0・1・8のどれかに落ちます。三の場合の物語の最初の一歩です。
2³=8を9で割った余りは8。4³=64なら余り1。もとの数が大きくても、小さな余りを比べて等式が無理だと分かる場合があります。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
9×7=63なので余り1。三乗した結果の余りを計算します。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
1。 9×7=63なので余り1。三乗した結果の余りを計算します。
時計は三乗を正直に保ちます:4³ = 64の余りは1、2³の余りは8。余り1と8から二つ選んで足すと、2・0・7しかできません。したがって三で割れない数の三乗は、等式の反対側に立つことができません。
Mathlib · db584cd · Three.lean
lemma cube_of_castHom_ne_zero {n : ZMod 9} :castHom (show 3 ∣ 9 by simp) (ZMod 3) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8 := byrevert n; decidelemma cube_of_not_dvd {n : ℤ} (h : ¬ 3 ∣ n) :(n : ZMod 9) ^ 3 = 1 ∨ (n : ZMod 9) ^ 3 = 8 := byapply cube_of_castHom_ne_zerorwa [map_intCast, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd]/-- If `a b c : ℤ` are such that `¬ 3 ∣ a * b * c`, then `a ^ 3 + b ^ 3 ≠ c ^ 3`. -/theorem fermatLastTheoremThree_case_1 {a b c : ℤ} (hdvd : ¬ 3 ∣ a * b * c) :a ^ 3 + b ^ 3 ≠ c ^ 3 := by
最初の補題がぜんぶのエンジンです:ZMod 9では、ZMod 3の世界で消えない余りの三乗は1か8。decideが九つの場合をまとめて確かめ、ソースも短く保たれます。二つ目の補題は同じ規則を、3で割れない整数nへ運びます。表示された定理の続きは抜粋の下にあります:積a * b * cを3で割れないという仮定が、a・b・cそれぞれの条件へと分けられます。
9を法とする三乗
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
三乗は、9の時計では0・1・8のどれかに落ちます。三の場合の物語の最初の一歩です。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
時計は三乗を正直に保ちます:4³ = 64の余りは1、2³の余りは8。余り1と8から二つ選んで足すと、2・0・7しかできません。したがって三で割れない数の三乗は、等式の反対側に立つことができません。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →