高校
互いに素な脚を持つ三つ組には、m² − n²と2mnのレシピがあります。
6、8、10は、3、4、5を全部2倍した組。共通の倍率を外すと基本の組になります。m=3、n=2をm²−n²、2mn、m²+n²に入れると5、12、13です。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
6=2×3、8=2×4、10=2×5。共通の倍率を外して、基本の組を見ます。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
すべての数を2倍した組。 6=2×3、8=2×4、10=2×5。共通の倍率を外して、基本の組を見ます。
二つの歯車の位置:m = 3、n = 2なら3 ^ 2 - 2 ^ 2 = 5と2 × 3 × 2 = 12——三つ組(5, 12, 13)。そしてm = 5、n = 4なら9と40:9 ^ 2 + 40 ^ 2 = 81 + 1600 = 1681 = 41 ^ 2.
Mathlib · db584cd · PythagoreanTriples.lean
/-- A primitive Pythagorean triple `x, y, z` is a Pythagorean triple with `x` and `y` coprime.Such a triple is “primitively classified” if there exist coprime integers `m, n` such that either* `x = m ^ 2 - n ^ 2` and `y = 2 * m * n`, or* `x = 2 * m * n` and `y = m ^ 2 - n ^ 2`.-/@[nolint unusedArguments]def IsPrimitiveClassified (_ : PythagoreanTriple x y z) :=∃ m n : ℤ,(x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
IsPrimitiveClassifiedは、互いに素で偶奇の違う整数m・nが存在し、脚の交換も許して二つの式で表せることを述べます。一意性は主張しません。(m,n)と(−m,−n)は同じ二つの式を与えるからです。指数4の降下では、まず(a ^ 2, b ^ 2, c)、次に(a, n, m)へ分類を適用します。Four.leanは、このファイルのcoprime_classification'を、必要な符号と偶奇の条件とともに使います。
整った三つ組は因子を持たない
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
互いに素な脚を持つ三つ組には、m² − n²と2mnのレシピがあります。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
二つの歯車の位置:m = 3、n = 2なら3 ^ 2 - 2 ^ 2 = 5と2 × 3 × 2 = 12——三つ組(5, 12, 13)。そしてm = 5、n = 4なら9と40:9 ^ 2 + 40 ^ 2 = 81 + 1600 = 1681 = 41 ^ 2.
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →