容疑者の内側の二つの直角三角形

Leanでの使用例・原文の抜粋

Mathlib · db584cd · Four.lean

154theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) : False := by155  -- Use the fact that a ^ 2, b ^ 2, c form a pythagorean triple to obtain m and n such that156  -- a ^ 2 = m ^ 2 - n ^ 2, b ^ 2 = 2 * m * n and c = m ^ 2 + n ^ 2157  -- first the formula:158  have ht : PythagoreanTriple (a ^ 2) (b ^ 2) c := by159    delta PythagoreanTriple160    linear_combination h.1.2.2161  -- coprime requirement:162  have h2 : Int.gcd (a ^ 2) (b ^ 2) = 1 :=163    Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal h).pow164  -- in order to reduce the possibilities we get from the classification of pythagorean triples165  -- it helps if we know the parity of a ^ 2 (and the sign of c):166  have ha22 : a ^ 2 % 2 = 1 := by167    rw [sq, Int.mul_emod, ha2]168    decide169  obtain ⟨m, n, ht1, ht2, ht3, ht4, ht5, ht6⟩ := ht.coprime_classification' h2 ha22 hc170  -- Now a, n, m form a pythagorean triple and so we can obtain r and s such that171  -- a = r ^ 2 - s ^ 2, n = 2 * r * s and m = r ^ 2 + s ^ 2172  -- formula:173  have htt : PythagoreanTriple a n m := by174    delta PythagoreanTriple175    linear_combination ht1176  -- a and n are coprime, because a ^ 2 = m ^ 2 - n ^ 2 and m and n are coprime.177  have h3 : Int.gcd a n = 1 := by178    apply Int.isCoprime_iff_gcd_eq_one.mp179    apply @IsCoprime.of_mul_left_left _ _ _ a180    rw [← sq, ht1, (by ring : m ^ 2 - n ^ 2 = m ^ 2 + -n * n)]181    exact (Int.isCoprime_iff_gcd_eq_one.mpr ht4).pow_left.add_mul_right_left (-n)

このLeanの読み方

htは等式そのものから三つ組を作ります——linear_combinationが目標の等式を三つ組の形へ組み替える、純粋な代数の帳簿です。分類には近くで用意された三つの事実が届きます:互いに素な脚(近くのcoprime_of_minimalのpow)、奇数である脚(ha22)、正の斜辺。同じ定理のさらに奥では、三つ組a・n・mにもう一度分類が適用されます——構造の入れ子こそ、降下法が食べるものです。