代数構造は型クラスで表す

Monoid M，Group G，Ring R，Field K などは型 M，G，R，K に入っている構造を表す型クラスです． 数学では「群 G」と言うことが多いですが，Lean では「型 G と，その上の群構造 [Group G]」を分けて書きます．

#check Monoid
#check CommMonoid
#check Group
#check AddCommGroup
#check Semiring
#check Ring
#check CommRing
#check Field

section BasicStructures

variable {M : Type*} [Monoid M]

example (x : M) : x * 1 = x := by
  simp

example (x y z : M) : (x * y) * z = x * (y * z) := by
  exact mul_assoc x y z

variable {A : Type*} [AddCommMonoid A]

example (x y : A) : x + y = y + x := by
  exact add_comm x y

end BasicStructures

Monoid は乗法的な記法を使います． 加法的に書きたい場合は AddMonoid や AddCommGroup を使います．

同じ数学的事実でも，乗法的な構造では mul_assoc，加法的な構造では add_assoc のように名前が分かれます．

section Groups

variable {G H : Type*} [Group G] [Group H]

example (x : G) : x * x⁻¹ = 1 := by
  simp

example (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
  group

example (f : G →* H) (x : G) : f (x⁻¹) = (f x)⁻¹ := by
  exact map_inv f x

end Groups

section AdditiveGroups

variable {A : Type*} [AddCommGroup A]

example (x y z : A) : z + x + (y - z - x) = y := by
  abel

end AdditiveGroups

group は群の公理から従う等式を解く tactic です． 加法可換群では abel が使えます． どちらも「代数構造の公理に従う正規化」を行うものだと考えるとよいです．