funlean.
順番 14 / 64

中学校

大きさだけを見る

絶対値|c|は大きさだけを見ます:ゼロからの距離です。

まず、身近な例で

数直線で−7も7も、0から7歩の場所にあります。絶対値はこの距離なので、|−7|=7です。

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

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

|−7|はいくつ？

答えと考え方を読む

7。 数直線で0からの距離を測ります。−7は7歩離れていて、距離は負にはなりません。

3段階で考えよう

  1. 符号つきの数には大きさが必要です:Int.natAbsは|c|、ゼロからの距離を読みます——−11も11も同じ11で、符号はわざと忘れます。
  2. 記録natAbsHomは機械とその約束を並べて保存します:map_mul'は|a × b| = |a| × |b|を、map_one'は|1| = 1を、map_zero'は|0| = 0を固定します。
  3. 大きさは掛け算で積み上がります——それがmap_mul'——だから降下は大きさで容疑者の順位をつけられます:各解のcを|c|という自然数へ置き換えれば、「より小さい容疑者」は「必ず見つかる最小の数」になります。

小さな例で確かめる

測ってから掛けます:|−7| = 7、|3| = 3。そして実際|−7 × 3| = |−21| = 21 = 7 × 3。大きさは符号を気にせず、ゼロからの距離だけを見ます。

Leanの定義・原文の抜粋

Mathlib · db584cd · NatAbs.lean

/-- `Int.natAbs` as a bundled `MonoidWithZeroHom`. -/@[simps]def natAbsHom : ℤ →*₀ ℕ where  toFun := Int.natAbs  map_mul' := Int.natAbs_mul  map_one' := Int.natAbs_one  map_zero' := Int.natAbs_zero

このLeanの読み方

natAbsHomは小さな機械の目録です:符号つき整数を食べて自然数を返し、各欄が束ねの約束を一つずつ証明します——掛け算・1・ゼロ。降下のページでは、解はまさにこの機械で順位づけられ(Minimalの定義はcのInt.natAbsを比べます)、「最小の容疑者」は文字どおり「最小の自然数」になります——その順位はいつまでも続けられません。

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

この言葉を使う章

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

ミカのたすけ舟

大きさだけを見る

今は、一つだけ

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

言葉をほどこう

絶対値|c|は大きさだけを見ます:ゼロからの距離です。

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

小さな手がかり

測ってから掛けます:|−7| = 7、|3| = 3。そして実際|−7 × 3| = |−21| = 21 = 7 × 3。大きさは符号を気にせず、ゼロからの距離だけを見ます。

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

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