class AlgebraInLean.Magma (α : Type u_1) : Type u_1

A magma is the simplest algebraic structure. It is a set along with a binary operation with no additional properties imposed

• op : α → α → α

def AlgebraInLean.μ {α : Type u_1} [AlgebraInLean.Magma α] : α → α → α

The operation on a Magma or derived structure

Equations

• AlgebraInLean.μ = AlgebraInLean.Magma.op

class AlgebraInLean.Semigroup (α : Type u_2) extends AlgebraInLean.Magma : Type u_2

A semigroup is a magma where the operation is associative

• op : α → α → α
• op_assoc : ∀ (a b c : α), AlgebraInLean.μ (AlgebraInLean.μ a b) c = AlgebraInLean.μ a (AlgebraInLean.μ b c)

theorem AlgebraInLean.Semigroup.op_assoc {α : Type u_2} [self : AlgebraInLean.Semigroup α] (a : α) (b : α) (c : α) : AlgebraInLean.μ (AlgebraInLean.μ a b) c = AlgebraInLean.μ a (AlgebraInLean.μ b c)

theorem AlgebraInLean.op_assoc {α : Type u_1} [AlgebraInLean.Semigroup α] (a : α) (b : α) (c : α) : AlgebraInLean.μ (AlgebraInLean.μ a b) c = AlgebraInLean.μ a (AlgebraInLean.μ b c)

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

class AlgebraInLean.Monoid (α : Type u_2) extends AlgebraInLean.Semigroup : Type u_2

A monoid is a semigroup with an identity element

• op : α → α → α
• op_assoc : ∀ (a b c : α), AlgebraInLean.μ (AlgebraInLean.μ a b) c = AlgebraInLean.μ a (AlgebraInLean.μ b c)
• id : α
• op_id : ∀ (a : α), AlgebraInLean.μ a AlgebraInLean.Monoid.id = a
• id_op : ∀ (a : α), AlgebraInLean.μ AlgebraInLean.Monoid.id a = a

theorem AlgebraInLean.Monoid.op_id {α : Type u_2} [self : AlgebraInLean.Monoid α] (a : α) : AlgebraInLean.μ a AlgebraInLean.Monoid.id = a

theorem AlgebraInLean.Monoid.id_op {α : Type u_2} [self : AlgebraInLean.Monoid α] (a : α) : AlgebraInLean.μ AlgebraInLean.Monoid.id a = a

def AlgebraInLean.𝕖 {α : Type u_1} [AlgebraInLean.Monoid α] : α

The identity element of a monoid or derived structure

Equations

• AlgebraInLean.𝕖 = AlgebraInLean.Monoid.id

theorem AlgebraInLean.op_id {α : Type u_1} [AlgebraInLean.Monoid α] (a : α) : AlgebraInLean.μ a AlgebraInLean.𝕖 = a

a ⬝ 𝕖 = a

theorem AlgebraInLean.id_op {α : Type u_1} [AlgebraInLean.Monoid α] (a : α) : AlgebraInLean.μ AlgebraInLean.𝕖 a = a

𝕖 ⬝ a = a

class AlgebraInLean.CommMonoid (α : Type u_2) extends AlgebraInLean.Monoid : Type u_2

Commutative monoids have the additional property that the operation is commutative

• op : α → α → α
• op_assoc : ∀ (a b c : α), AlgebraInLean.μ (AlgebraInLean.μ a b) c = AlgebraInLean.μ a (AlgebraInLean.μ b c)
• id : α
• op_id : ∀ (a : α), AlgebraInLean.μ a AlgebraInLean.Monoid.id = a
• id_op : ∀ (a : α), AlgebraInLean.μ AlgebraInLean.Monoid.id a = a
• op_comm : ∀ (a b : α), AlgebraInLean.μ a b = AlgebraInLean.μ b a

theorem AlgebraInLean.CommMonoid.op_comm {α : Type u_2} [self : AlgebraInLean.CommMonoid α] (a : α) (b : α) : AlgebraInLean.μ a b = AlgebraInLean.μ b a

theorem AlgebraInLean.op_comm {α : Type u_1} [AlgebraInLean.CommMonoid α] (a : α) (b : α) : AlgebraInLean.μ a b = AlgebraInLean.μ b a

a ⬝ b = b ⬝ a

class AlgebraInLean.Group (α : Type u_2) extends AlgebraInLean.Monoid : Type u_2

A group is a monoid with inverses

• op : α → α → α
• op_assoc : ∀ (a b c : α), AlgebraInLean.μ (AlgebraInLean.μ a b) c = AlgebraInLean.μ a (AlgebraInLean.μ b c)
• id : α
• op_id : ∀ (a : α), AlgebraInLean.μ a AlgebraInLean.Monoid.id = a
• id_op : ∀ (a : α), AlgebraInLean.μ AlgebraInLean.Monoid.id a = a
• inv : α → α
• inv_op : ∀ (a : α), AlgebraInLean.μ (AlgebraInLean.Group.inv a) a = AlgebraInLean.𝕖

theorem AlgebraInLean.Group.inv_op {α : Type u_2} [self : AlgebraInLean.Group α] (a : α) : AlgebraInLean.μ (AlgebraInLean.Group.inv a) a = AlgebraInLean.𝕖

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

The inverse map of a group or derived structure

Equations

• AlgebraInLean.ι = AlgebraInLean.Group.inv

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

a⁻¹ ⬝ a = 𝕖

class AlgebraInLean.AbelianGroup (G : Type u_2) extends AlgebraInLean.Group : Type u_2

An abelian group is a group with commutativity

• op : G → G → G
• op_assoc : ∀ (a b c : G), AlgebraInLean.μ (AlgebraInLean.μ a b) c = AlgebraInLean.μ a (AlgebraInLean.μ b c)
• id : G
• op_id : ∀ (a : G), AlgebraInLean.μ a AlgebraInLean.Monoid.id = a
• id_op : ∀ (a : G), AlgebraInLean.μ AlgebraInLean.Monoid.id a = a
• inv : G → G
• inv_op : ∀ (a : G), AlgebraInLean.μ (AlgebraInLean.Group.inv a) a = AlgebraInLean.𝕖
• op_comm : ∀ (a b : G), AlgebraInLean.μ a b = AlgebraInLean.μ b a

instance AlgebraInLean.instCommMonoidOfAbelianGroup {α : Type u_1} [AlgebraInLean.AbelianGroup α] : AlgebraInLean.CommMonoid α

Equations

• AlgebraInLean.instCommMonoidOfAbelianGroup = AlgebraInLean.CommMonoid.mk ⋯

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

a ⬝ a⁻¹ = 𝕖

theorem AlgebraInLean.op_left_cancel {α : Type u_1} [AlgebraInLean.Group α] (a : α) (b : α) (c : α) (h : AlgebraInLean.μ a b = AlgebraInLean.μ a c) : b = c

a ⬝ b = a ⬝ c ⇒ b = c

theorem AlgebraInLean.op_right_cancel {α : Type u_1} [AlgebraInLean.Group α] (a : α) (b : α) (c : α) (h : AlgebraInLean.μ b a = AlgebraInLean.μ c a) : b = c

b ⬝ a = c ⬝ a ⇒ b = c