証明レベル
ある重さとレベルの空間では、すべてのカスプ形式が0だと定理で示します。
入れてよい関数がゼロの関数だけなら、箱は空ではなく{0}です。でも、0ではない関数は入っていません。「空の箱」と「0だけの箱」は違います。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
空の箱と、0と書いた札が一枚ある箱を区別しよう。消滅の議論が除くのは、0ではない形式です。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
いいえ、0はあるが、0でないものはない。 空の箱と、0と書いた札が一枚ある箱を区別しよう。消滅の議論が除くのは、0ではない形式です。
零関数もカスプ形式なので、この空間は無ではありません。要素が一つの集合{0}です。議論が求める0ではない形式が、ただ存在しないだけです。
FLT · aa2d8b3 · Thm_ModularForm_S2_Gamma0_2_eq_zero.lean
theorem ModularForm.S2_Gamma0_2_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) : f = 0 := by p2m_exact_reverting @_root_.P2MW.S_ModularForm_S2_Gamma0_2_eq_zero.solution型の名前がレベルと重さの両方を固定します。証明項は上流プロジェクトの別途検査された解に委ねる手法で、このページは主張を表示するだけで、大きな議論を再実行しません。
誰もいない部屋
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
ある重さとレベルの空間では、すべてのカスプ形式が0だと定理で示します。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
零関数もカスプ形式なので、この空間は無ではありません。要素が一つの集合{0}です。議論が求める0ではない形式が、ただ存在しないだけです。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →