大学
仮の解を、λがcを割る回数で順位づけると、いちばん小さいものが必ずあります。
正の整数の番号札が一枚でもあれば、その中に一番小さい番号があります。それを選んだ後で、さらに小さい有効な番号札を作れたら、「一番小さい」と矛盾します。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
最小は、並べた順ではなく大きさで決めます。さらに小さい有効な候補を作れたら、最小だったことと矛盾します。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
6。 最小は、並べた順ではなく大きさで決めます。さらに小さい有効な候補を作れたら、最小だったことと矛盾します。
容疑者を記録で順位づけます:仮の解の中から、cの中のλの回数がいちばん小さいものを選びます。いつでも真に小さい回数を作れるなら、そもそも最小の記録は存在できません。
Mathlib · db584cd · Three.lean
/-- We say that `S : Solution` is minimal if for all `S₁ : Solution`, the multiplicity of `λ` in`S.c` is less or equal than the multiplicity in `S₁.c`. -/def Solution.isMinimal : Prop := ∀ (S₁ : Solution hζ), S.multiplicity ≤ S₁.multiplicityomit [NumberField K] [IsCyclotomicExtension {3} ℚ K] ininclude S in/-- If there is a solution then there is a minimal one. -/lemma Solution.exists_minimal : ∃ (S₁ : Solution hζ), S₁.isMinimal := by
定義が目盛りです:解どうしをcの中のλの重複度で比べ、その数がいちばん小さい解を最小と呼びます。補題の前の二行の指令は、まわりの型クラスの仮定を削り、Sを明示的に割り当てます。この主張には構造の欄だけが要ります。抜粋の下では、証明本体がすべての解の重複度を空でない自然数の族として集め、その最小元を読み取ります。
いちばん小さい解を選ぶ
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
仮の解を、λがcを割る回数で順位づけると、いちばん小さいものが必ずあります。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
容疑者を記録で順位づけます:仮の解の中から、cの中のλの回数がいちばん小さいものを選びます。いつでも真に小さい回数を作れるなら、そもそも最小の記録は存在できません。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →