theorem AlgebraInLean.id_unique {α : Type u_1} [AlgebraInLean.Monoid α] (e₂ : α) (h : ∀ (a : α), AlgebraInLean.μ a e₂ = a ∧ AlgebraInLean.μ e₂ a = a) : e₂ = AlgebraInLean.𝕖

Uniqueness of the identity element in a monoid. If any element e₂ "behaves like" the identity, then it must be equal to the identity.

theorem AlgebraInLean.inv_unique {α : Type u_1} [AlgebraInLean.Group α] (a : α) (i : α) (h : AlgebraInLean.μ a i = AlgebraInLean.𝕖 ∧ AlgebraInLean.μ i a = AlgebraInLean.𝕖) : i = AlgebraInLean.ι a

Uniqueness of the inverse of an element. If any element i "behaves like" the inverse of a, then it must be equal to the inverse of a.

theorem AlgebraInLean.id_unique_left {α : Type u_1} [AlgebraInLean.Monoid α] (e₂ : α) (h : ∀ (a : α), AlgebraInLean.μ e₂ a = a) : e₂ = AlgebraInLean.𝕖

If any element e₂ is a left identity, then it is equal to the identity

theorem AlgebraInLean.id_unique_right {α : Type u_1} [AlgebraInLean.Monoid α] (e₂ : α) (h : ∀ (a : α), AlgebraInLean.μ a e₂ = a) : e₂ = AlgebraInLean.𝕖

If any element e₂ is a right identity, then it is equal to the identity

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

If any element i is a left inverse of a, then it is equal to the inverse of a

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

If any element i is a right inverse of a, then it is equal to the inverse of a

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

Colloquially, the "shoes and socks theorem" because you put on your socks before your shoes, but you take off your shoes before your socks. "Anticommutativity" is the fancy name for this: a function that "commutes" with the operation but inverts the order of the operands.

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

The inverse of the inverse of an element is itself

theorem AlgebraInLean.inv_id {α : Type u_1} [AlgebraInLean.Group α] : AlgebraInLean.ι AlgebraInLean.𝕖 = AlgebraInLean.𝕖

The inverse of the identity element is the identity element