funlean.
順番 21 / 64

高校

辺が整数の直角三角形

ピタゴラス数:3・4・5の家族で、x² + y² = z²が成り立ちます。

まず、身近な例で

直角三角形の辺が3、4、5なら、3²+4²=5²。三つの辺が整数という条件と、直角になる等式を両方見ます。好きな整数三つでよいわけではありません。

ちいさな確認：考えてみよう

上の具体例を見ながら考えよう。何度やり直しても大丈夫。

3、4、5は直角三角形の等式を満たす？

答えと考え方を読む

はい、9+16=25。 足すのは辺の長さそのものではなく、その平方です。3²+4²=5²を確かめよう。

3段階で考えよう

  1. ピタゴラス数は、直角三角形に座る三つの整数です。定義はちょうど一行しか使いません:PythagoreanTriple x y zは、x * x + y * y = z * zという意味にすぎません。
  2. 家族を確かめます:3 ^ 2 + 4 ^ 2 = 9 + 16 = 25 = 5 ^ 2。だから(3, 4, 5)は三つ組で、全部を2倍した(6, 8, 10)も三つ組です。
  3. 脚は入れ替え可能です:pythagoreanTriple_commはxとyを交換します——x * x + y * y = y * y + x * xだから。証明はdeltaで一行の定義を開いて、次にrw [add_comm]。

小さな例で確かめる

(5, 12, 13)も家族に入ります:25 + 144 = 169。ここでは「図」と「等式」が同じ言葉です——一行の定義の静かな力です。

Leanの定義・原文の抜粋

Mathlib · db584cd · PythagoreanTriples.lean

/-- Three integers `x`, `y`, and `z` form a Pythagorean triple if `x * x + y * y = z * z`. -/def PythagoreanTriple (x y z : ℤ) : Prop :=  x * x + y * y = z * z /-- Pythagorean triples are interchangeable, i.e `x * x + y * y = y * y + x * x = z * z`.This comes from additive commutativity. -/theorem pythagoreanTriple_comm {x y z : ℤ} : PythagoreanTriple x y z ↔ PythagoreanTriple y x z := by  delta PythagoreanTriple  rw [add_comm]

このLeanの読み方

隠れた機械はありません:述語は整数についての一行の等式で、下の行にあるeq・symm・mulはその上に直接築かれます。前のページは四乗を二乗にたたんだので、a⁴ + b⁴ = c²はまさにこの形——PythagoreanTriple (a ^ 2) (b ^ 2) c——に着地します。脚がそれぞれ平方である直角三角形。3・4・5の学校の図へ降りることは、指数4の場合がその小さな容疑者を作り始める入口そのものです。

元の原文 ↗ · L42–50保存した原文全体を開く

この言葉を使う章

7. ベテランたちの事件簿
わからない・道に迷った

ミカのたすけ舟

辺が整数の直角三角形

今は、一つだけ

まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。

言葉をほどこう

ピタゴラス数:3・4・5の家族で、x² + y² = z²が成り立ちます。

このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。

小さな手がかり

(5, 12, 13)も家族に入ります:25 + 144 = 169。ここでは「図」と「等式」が同じ言葉です——一行の定義の静かな力です。

閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。

最初の小さな物語から読む →