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.
Binary operation on a set; associativity, commutativity, and a subset closed under the operation
Definition
A binary operation on a set is a function (A function is a relation with and implying ; , the value , domain and codomain) whose domain is the Cartesian product (The Cartesian product ),
written in infix form . That the value always lies in is part of the definition, and is referred to as being closed under . The pair is called a set equipped with a binary operation.
The operation is
- associative when for all ;
- commutative when for all .
Two elements commute when ; so is commutative exactly when every two elements of commute.
A subset is closed under when for all . In that case the restriction of to has all its values in and is therefore a binary operation on , called the restricted operation or the operation induced on ; it is again associative if is, and again commutative if is, since both conditions are equations required of elements of , which are in particular elements of .
Remarks
-
Notation. Where no confusion arises the operation is written multiplicatively, for , and additively, , when it is commutative and the context is additive. Nothing in this page depends on the choice: every statement is about an abstract operation.
-
Bracketing. Associativity is stated for three factors only. That it lets brackets be dropped in a product of any finite length is a theorem, not a restatement: it is Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either, proved below.
-
Familiar instances already in the library are addition and multiplication on (Addition of natural numbers, Multiplication of natural numbers), on (Arithmetic on the integers) and on any field (Field).