How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Left identity, right identity, and two-sided identity for a binary operation
Definition
Let be a binary operation on a set (Binary operation on a set; associativity, commutativity, and a subset closed under the operation) and let . Then is
- a left identity for when for every ;
- a right identity for when for every ;
- a two-sided identity, or simply an identity, when it is both.
Remarks
-
The three notions are genuinely different for a general operation, and the library keeps them apart deliberately: several existing items prove the two sides separately. For addition on , for instance, holds by the defining recursion (Addition of natural numbers) while is a theorem proved by induction (Left identity for addition).
-
A structure can have many left identities and no right identity, so "the identity" is not legitimate language until uniqueness is available. That is A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity, proved next, and it is the item that licenses the definite article everywhere below.
Depends on
Used by
- (gh)ⁿ = gⁿhⁿ fails without commutativity: two transpositions in Sym({1,2,3}) with (gh)² ≠ g²h² Counterexample
- A commutative monoid in which cancellation holds need not be a group: (ℕ, +) Counterexample
- In the multiplicative monoid H = {1, 4, 7, 10, …} of positive integers one more than a multiple of 3, the element 100 has two genuinely different factorisations into irreducibles, 4 · 25 and 10 · 10 Counterexample
- Group and abelian group Definition
- Left inverse, right inverse, and invertible element of a monoid Definition
- Monoid homomorphism and group homomorphism Definition
- Ring homomorphism: additive, multiplicative, and required to send 1 to 1 Definition
- Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides Definition
- Semigroup and monoid Definition
- Subgroup Definition
- Subring: a subset containing 1_R and closed under addition, additive inverses and multiplication Definition
- The quaternions ℍ: real quadruples with componentwise addition and an explicit multiplication formula matching the table on 1, i, j, k Definition
- The symmetric group Sym(X): the bijections of a set X under composition Definition
- Vector space over a field Definition
- (ℤ, +) is an abelian group, (ℤ, ·) is a commutative monoid that is not a group, and its group of units is {1, -1} Example
- For any field F, (F, +) and (F ∖ {0}, ·) are abelian groups; in particular (ℚ, +), (ℚ ∖ {0}, ·), (ℝ, +) and (ℝ ∖ {0}, ·) Example
- For n ≥ 1 the congruence classes modulo n form an abelian group (ℤ/n, +) of order n, generated by the class of 1 Example
- (ℤ, ·, 1) is a commutative monoid whose group of units is {1, -1}; equivalently u ∣ 1 holds exactly for u = 1 and u = -1 Lemma
- A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity Lemma
- Cancellation in a group: gx = gy or xg = yg forces x = y; equivalently left and right translation by g are bijections of G, so gx = h and xg = h each have exactly one solution Lemma
- In a group e⁻¹ = e, (g⁻¹)⁻¹ = g and (gh)⁻¹ = h⁻¹g⁻¹, the order of the last product being essential Lemma
- In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided Lemma
- In any ring 0 · a = a · 0 = 0, (-a)b = a(-b) = -(ab), (-a)(-b) = ab, (-1)a = -a and a(b - c) = ab - ac Lemma
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 11 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Identity element (Wikipedia) (standard reference, not scraped)