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.
Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides
Definition
A ring is a set carrying two binary operations (Binary operation on a set; associativity, commutativity, and a subset closed under the operation), addition and multiplication , and two distinguished elements and of , such that
- (R1) is an abelian group (Group and abelian group): addition is associative and commutative, for every , and every has an additive inverse;
- (R2) is a monoid (Semigroup and monoid): multiplication is associative and for every ;
- (R3) multiplication distributes over addition on both sides: for all ,
We write for , call the zero and the identity (or unity) of , write for the additive inverse of , and abbreviate .
Why "the" zero, "the" identity and "the" additive inverse are legitimate. Each of and is a two-sided identity for its own operation, and a binary operation has at most one two-sided identity (A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity, Left identity, right identity, and two-sided identity for a binary operation), so each is determined by the operation and the notation is single-valued. An additive inverse of is an inverse in the monoid (Left inverse, right inverse, and invertible element of a monoid), and in a monoid an element has at most one inverse (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); so names one element, and a single equation already forces .
Convention: a ring has an identity. Axiom (R2) asks for a monoid, so the existence of is part of the definition and is not an extra hypothesis to be carried around. This is the convention used throughout this library. A structure satisfying (R1), (R3) and the associativity half of (R2), but not required to have a multiplicative identity, is called a non-unital ring (also rng); it is not called a ring here, and where such a structure occurs it is named as a non-unital ring in as many words. The distinction has content: the companion page exhibits a subset of that is closed under addition, additive inverses and multiplication and is not a subring, precisely because it misses the identity.
Nothing above requires . A ring in which has exactly one element; the companion page records it as the zero ring. Definitions that need — integral domain, division ring, field — say so explicitly.
Remarks
-
Both distributive laws are stated, and neither is redundant here. Multiplication is not assumed commutative, so does not follow from . The published Field states only the left form, in a setting where multiplication is commutative; a ring is not that setting. The quaternions (The quaternions : real quadruples with componentwise addition and an explicit multiplication formula matching the table on ), constructed on this page, are a ring whose multiplication is not commutative, so for them the two laws are genuinely two statements and both are checked.
-
A ring packages two structures the library already has. Read (R1) alone and a ring is an abelian group; read (R2) alone and it is a monoid. Every theorem proved about groups and about monoids therefore applies to a ring without restatement, and this page uses that repeatedly rather than reproving cancellation, uniqueness of inverses, or the behaviour of finite products.
-
Notation for repeated addition. For and the expression means the integer power of in the additive group , written additively as in Powers : natural exponents in a monoid and integer exponents in a group, with . It is not a product formed with the ring multiplication: is an external integer scalar, even when the underlying set of happens to contain integers. The arithmetic of these multiples is Integer multiples in a ring: , , and for all and .
Depends on
Group and abelian group
Semigroup and monoid
Binary operation on a set; associativity, commutativity, and a subset closed under the operation
Left identity, right identity, and two-sided identity for a binary operation
A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity
Left inverse, right inverse, and invertible element of a monoid
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