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.
Subgroup
Definition
Let be a group (Group and abelian group) with identity . A subset is a subgroup of , written , when
- (S1) ;
- (S2) is closed under the operation: implies (Binary operation on a set; associativity, commutativity, and a subset closed under the operation);
- (S3) is closed under inverses: implies .
By (S2) the operation of restricts to a binary operation on ; it is associative there because it is associative on , the element of (S1) is a two-sided identity for it (Left identity, right identity, and two-sided identity for a binary operation), and (S3) supplies for each a two-sided inverse lying in (Left inverse, right inverse, and invertible element of a monoid). So a subgroup, with the restricted operation, is itself a group, and its identity and its inverses are those of .
Every group has the two trivial subgroups and itself; a subgroup with is called proper.
Definition references
Remarks
-
The definition is stated so that no comparison of structures is needed. A subgroup is a subset satisfying three closure conditions, and the group structure it carries is inherited rather than chosen. The converse reading, that a subset which happens to be a group under the restricted operation is a subgroup in the above sense, is a small theorem rather than a tautology, because a priori such a subset could carry a different identity; it is part of One-step subgroup test: a nonempty is a subgroup iff for all ; the identity and the inverses of are then those of , and cancellation in is what rules that out.
-
Conditions (S1)–(S3) are not independent as stated: if is nonempty and satisfies (S2) and (S3) then it satisfies (S1). The economical single test is One-step subgroup test: a nonempty is a subgroup iff for all ; the identity and the inverses of are then those of .
-
Intersections of subgroups are subgroups (The intersection of a nonempty family of subgroups of is a subgroup of ), which is what makes "the smallest subgroup containing a given subset" meaningful (The subgroup generated by a subset, the cyclic subgroup , and cyclic groups). Unions of subgroups are almost never subgroups.