class AlgebraInLean.GroupIntro.Group (G : Type u_1) : Type u_1

The most common structure in algebra is the group. A group is defined as a set G along with some binary operation on that set that satisfies some properties (listed below). This is represented in Lean as a type class, which are objects that share certain properties (a proof that a type satisfies a given type class is called an instance). For a given type G, the type Group G corresponds to it being a group; as an argument, this is often written [Group G], which makes Lean automatically look for an implementation of such.

• op : G → G → G

  The group operation as a binary function. This type signature implies that it is necessarily closed.

• op_assoc : ∀ (a b c : G), AlgebraInLean.GroupIntro.Group.op (AlgebraInLean.GroupIntro.Group.op a b) c = AlgebraInLean.GroupIntro.Group.op a (AlgebraInLean.GroupIntro.Group.op b c)

  (a ⬝ b) ⬝ c = a ⬝ (b ⬝ c)

• id : G

  The identity element of the group (denoted "𝕖"), with properties described below

• op_id : ∀ (a : G), AlgebraInLean.GroupIntro.Group.op a AlgebraInLean.GroupIntro.Group.id = a

  a ⬝ 𝕖 = a

• id_op : ∀ (a : G), AlgebraInLean.GroupIntro.Group.op AlgebraInLean.GroupIntro.Group.id a = a

  𝕖 ⬝ a = a

• inv : G → G

  For x : G, inv x is its inverse, with the property described below

• inv_op : ∀ (a : G), AlgebraInLean.GroupIntro.Group.op (AlgebraInLean.GroupIntro.Group.inv a) a = AlgebraInLean.GroupIntro.Group.id

  a⁻¹ ⬝ a = 𝕖

theorem AlgebraInLean.GroupIntro.Group.op_assoc {G : Type u_1} [self : AlgebraInLean.GroupIntro.Group G] (a : G) (b : G) (c : G) : AlgebraInLean.GroupIntro.Group.op (AlgebraInLean.GroupIntro.Group.op a b) c = AlgebraInLean.GroupIntro.Group.op a (AlgebraInLean.GroupIntro.Group.op b c)

(a ⬝ b) ⬝ c = a ⬝ (b ⬝ c)

theorem AlgebraInLean.GroupIntro.Group.op_id {G : Type u_1} [self : AlgebraInLean.GroupIntro.Group G] (a : G) : AlgebraInLean.GroupIntro.Group.op a AlgebraInLean.GroupIntro.Group.id = a

a ⬝ 𝕖 = a

theorem AlgebraInLean.GroupIntro.Group.id_op {G : Type u_1} [self : AlgebraInLean.GroupIntro.Group G] (a : G) : AlgebraInLean.GroupIntro.Group.op AlgebraInLean.GroupIntro.Group.id a = a

𝕖 ⬝ a = a

theorem AlgebraInLean.GroupIntro.Group.inv_op {G : Type u_1} [self : AlgebraInLean.GroupIntro.Group G] (a : G) : AlgebraInLean.GroupIntro.Group.op (AlgebraInLean.GroupIntro.Group.inv a) a = AlgebraInLean.GroupIntro.Group.id

a⁻¹ ⬝ a = 𝕖

def AlgebraInLean.GroupIntro.μ {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] : G → G → G

The group operation

Equations

• AlgebraInLean.GroupIntro.μ = AlgebraInLean.GroupIntro.Group.op

theorem AlgebraInLean.GroupIntro.op_assoc {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] (a : G) (b : G) (c : G) : AlgebraInLean.GroupIntro.μ (AlgebraInLean.GroupIntro.μ a b) c = AlgebraInLean.GroupIntro.μ a (AlgebraInLean.GroupIntro.μ b c)

(a ⬝ b) ⬝ c = a ⬝ (b ⬝ c)

def AlgebraInLean.GroupIntro.𝕖 {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] : G

The identity element of the group

Equations

• AlgebraInLean.GroupIntro.𝕖 = AlgebraInLean.GroupIntro.Group.id

theorem AlgebraInLean.GroupIntro.op_id {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] (a : G) : AlgebraInLean.GroupIntro.μ a AlgebraInLean.GroupIntro.𝕖 = a

a ⬝ 𝕖 = a

theorem AlgebraInLean.GroupIntro.id_op {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] (a : G) : AlgebraInLean.GroupIntro.μ AlgebraInLean.GroupIntro.𝕖 a = a

𝕖 ⬝ a = a

def AlgebraInLean.GroupIntro.ι {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] : G → G

The inverse map of the group

Equations

• AlgebraInLean.GroupIntro.ι = AlgebraInLean.GroupIntro.Group.inv

theorem AlgebraInLean.GroupIntro.inv_op {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] (a : G) : AlgebraInLean.GroupIntro.μ (AlgebraInLean.GroupIntro.ι a) a = AlgebraInLean.GroupIntro.𝕖

a⁻¹ ⬝ a = 𝕖

theorem AlgebraInLean.GroupIntro.op_inv {G : Type u_1} [AlgebraInLean.GroupIntro.Group G] (a : G) : AlgebraInLean.GroupIntro.μ a (AlgebraInLean.GroupIntro.ι a) = AlgebraInLean.GroupIntro.𝕖

a ⬝ a⁻¹ =𝕖