型クラスで一般化された定理を読む¶
Mathlib の定理は，特定の型だけではなく，型クラスで一般化された形で書かれることがよくあります．
たとえば add_comm は自然数専用の定理ではなく，足し算が可換な任意の型で使える定理です．
#check add_comm の結果を見ると，必要な型クラス仮定が明示されます．
#check add_comm
#check add_zero
#check le_total
section GenericAlgebra
variable {α : Type*} [AddCommMonoid α]
example (a b : α) : a + b = b + a := by
exact add_comm a b
example (a : α) : a + 0 = a := by
exact add_zero a
end GenericAlgebra
角括弧 [AddCommMonoid α] は，「α には加法可換モノイド構造がある」というインスタンスを要求します．
Lean はこの仮定を使って + や 0 の意味を決め，add_comm や add_zero を適用します．
実際には add_comm だけならより弱い AddCommMagma で十分ですが，ここでは add_zero も同じ section で使うため AddCommMonoid を仮定しています．
Type* は universe レベルを Lean に推論させる notation で，Type u の universe 変数を明示しない書き方です．
Chapter 02 で見た LE や Add と同じく，Mathlib の AddCommMonoid や LinearOrder も型クラスです．
違いは，Mathlib ではそれらが階層化され，多くの演算・法則・notation・補題をまとめて利用できるようになっている点です．
section GenericOrder
variable {α : Type*} [LinearOrder α]
example (a b : α) : a ≤ b ∨ b ≤ a := by
exact le_total a b
end GenericOrder
このように，Mathlib の多くの定理は「型 α と，その型に入っている構造」を分けて書きます．
後半の章で現れる Group，Ring，TopologicalSpace，Module なども同じ発想です．