長めの例: ℤ を ℚ の加法部分群として作る

紙の数学では「整数全体は有理数の加法部分群である」と簡単に書きます． Lean では，これを AddSubgroup ℚ の項として作ります．

ポイントは次の通りです．

• 台集合は Set.range ((↑) : ℤ → ℚ) として表す．
• 0 が入ることを示す．
• 加法で閉じていることを示す．
• 負元で閉じていることを示す．

この例は，部分構造が「集合 + 閉性の証明」であることを具体的に示しています．

def integersInRationals : AddSubgroup ℚ where
  carrier := Set.range ((↑) : ℤ → ℚ)
  zero_mem' := by
    use 0
    norm_num
  add_mem' := by
    rintro _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
    use m + n
    norm_num
  neg_mem' := by
    rintro _ ⟨m, rfl⟩
    use -m
    norm_num

example : (3 : ℚ) ∈ integersInRationals := by
  use (3 : ℤ)
  norm_num

example : (1 / 2 : ℚ) ∉ integersInRationals := by
  rintro ⟨z, hz⟩
  have htwo : ((2 * z : ℤ) : ℚ) = 1 := by
    norm_num [Int.cast_mul, hz]
  have hInt : (2 * z : ℤ) = 1 := by
    exact_mod_cast htwo
  omega

最後の例は少し人工的ですが，「Set.range の元である」という仮定を ∃ z : ℤ, ... として取り出し，整数性の情報を使って矛盾を出しています．

代数の形式化では，このように「集合としての記述」と「構造としての記述」を行き来することがよくあります．