中学校
正方形になる数は、4の時計で0か1に座ります。2には決して座りません。
0、1、2、3を二乗して4で割ると、余りは0、1、0、1です。規則が見えてきますね。ずっと続く理由は、証明で確かめます。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
5²=25=4×6+1です。一例を計算することと、平方すべてについての主張を証明することは別です。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
1。 5²=25=4×6+1です。一例を計算することと、平方すべてについての主張を証明することは別です。
自分でも確かめよう。5 ^ 2 = 25 = 6 × 4 + 1の余りは1、6 ^ 2 = 36 = 9 × 4の余りは0。整数の平方を4で割った余りは、2にはなりません。
Mathlib · db584cd · PythagoreanTriples.lean
theorem sq_ne_two_fin_zmod_four (z : ZMod 4) : z * z ≠ 2 := bychange Fin 4 at zfin_cases z <;> decidetheorem Int.sq_ne_two_mod_four (z : ℤ) : z * z % 4 ≠ 2 := bysuffices ¬z * z % (4 : ℕ) = 2 % (4 : ℕ) by exact thisrw [← ZMod.intCast_eq_intCast_iff']simpa using sq_ne_two_fin_zmod_four _
4の時計では、偶数は2 · 2 = 4なので平方すると0になり、奇数は常に偶数の2倍より1大きいので(奇数 × 奇数は4の倍数プラス1)、平方すると1になります。最初の証明は有限の時計を総当たりで確かめる、学校の表が作るのと同じ国勢調査です。二番目の証明は、時計型を一度通ることで(rw [← ZMod.intCast_eq_intCast_iff'])、この事実を整数の余りの言葉へ持ち上げます。ファイルは、一行の事実のために小さな場合分けの代償を払うことがあります。
4の時計と平方数
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
正方形になる数は、4の時計で0か1に座ります。2には決して座りません。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
自分でも確かめよう。5 ^ 2 = 25 = 6 × 4 + 1の余りは1、6 ^ 2 = 36 = 9 × 4の余りは0。整数の平方を4で割った余りは、2にはなりません。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →