大学
降下のために、単元uのかかったもっと大きな主張を、まず証明します。
x³+y³をx³−y³にすれば、符号という条件が変わります。一般化した主張では、許される係数の変化を式の中に記録します。元の式と同じだと決めつけません。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
x=y=1なら、前者は2、後者は0です。一般化した主張でも、どんな係数を許すかを正確に指定します。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
いいえ、許される係数の変化として記録する。 x=y=1なら、前者は2、後者は0です。一般化した主張でも、どんな係数を許すかを正確に指定します。
単元とは、逆数を持つ元です。普通の整数では1と−1だけ。広い主張は、このような係数の動きを許します。音量は変わっても旋律は変わらない、という許し方です。
Mathlib · db584cd · Three.lean
/-- `FermatLastTheoremForThreeGen` is the statement that `a ^ 3 + b ^ 3 = u * c ^ 3` has nonontrivial solutions in `𝓞 K` for all `u : (𝓞 K)ˣ` such that `¬ λ ∣ a`, `¬ λ ∣ b` and `λ ∣ c`.The reason to consider `FermatLastTheoremForThreeGen` is to make a descent argument working. -/def FermatLastTheoremForThreeGen : Prop :=∀ a b c : 𝓞 K, ∀ u : (𝓞 K)ˣ, c ≠ 0 → ¬ λ ∣ a → ¬ λ ∣ b → λ ∣ c → IsCoprime a b →a ^ 3 + b ^ 3 ≠ u * c ^ 3/-- To prove `FermatLastTheoremFor 3`, it is enough to prove `FermatLastTheoremForThreeGen`. -/lemma FermatLastTheoremForThree_of_FermatLastTheoremThreeGen[NumberField K] [IsCyclotomicExtension {3} ℚ K] :FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3 := by
まず説明文から読みます。より広い主張が存在する理由をはっきり言っています——降下法を働かせるためです。定義は条件を列挙します:c ≠ 0、λはa・bを割らない、λはcを割る、aとbは互いに素。λ ∣ cという条件は前のページの場合分けの対応物です:3で割れる事がどれか一つの数に落ち、議論がそれをcに整えます。
単元つきのより広い網
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
降下のために、単元uのかかったもっと大きな主張を、まず証明します。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
単元とは、逆数を持つ元です。普通の整数では1と−1だけ。広い主張は、このような係数の動きを許します。音量は変わっても旋律は変わらない、という許し方です。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →