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.
For prime ,
Statement
For every prime , See Group isomorphisms, automorphisms and the set .
Facts & Assumptions
Given: The hypotheses and objects in the Statement.
An isomorphism is a bijective group homomorphism; an automorphism is an isomorphism from a group to itself, and (Group isomorphisms, automorphisms and the set ).
Let and be groups. Their external direct product has underlying set and componentwise operation The fact that this operation makes a group, with the indicated identity and inverses, is proved in thm-external-direct-product-is-a-group. Until that result is used, this definition introduces only the set and its componentwise binary operation. (The external direct product with componentwise multiplication).
For groups and , the componentwise operation of def-external-direct-product-of-groups makes a group. Its identity is , and Moreover the coordinate maps and are group homomorphisms. ( is a group with identity , coordinatewise inverses, and homomorphic coordinate projections).
For every prime , the operations of addition and multiplication on make it a field (def-field). (For every prime , the two operations on make it a field).
Let be a positive integer. Every class in (def-integers-modulo-n) contains exactly one integer with . Consequently the map is a bijection from the von Neumann natural to , and . This includes , where the only representative is . For , the map is a bijection . (For , every class in has one representative with , so ; while is in bijection with ).
- If and are finite then is finite and (def-finite-cardinality). 2. Let and let be finite sets. Write Then is finite and , the right-hand product being the -valued one of def-nat-finite-sum-and-product. (The product rule: , and ).
Let be a finite set (def-countable) and let . Then: 1. is finite; 2. (def-finite-cardinality); 3. if and only if ; 4. every injection is a bijection, and every surjection is a bijection. (A subset of a finite set is finite, with , and equality holds if and only if ).
For a subset of a group , the generated subgroup is the smallest subgroup of containing . (The subgroup generated by a subset, the cyclic subgroup , and cyclic groups).
Proof
In the additive group , a homomorphism is determined by the images and of the two coordinate generators, because every element has a unique coordinate expression.
If or , the image is a proper cyclic subgroup. If and , the elements of each coset are disjoint as varies, so generate all elements and the homomorphism is bijective.
There are choices for nonzero . Its cyclic subgroup has exactly elements, leaving choices for ; multiplication gives automorphisms.
When , the same count gives ; the argument is entirely in coordinates and makes no matrix-group identification. This proves the stated claim.
Depends on
- Group isomorphisms, automorphisms and the set $\operatorname{Aut}(G)$
- The external direct product $G\times H$ with componentwise multiplication
- $G\times H$ is a group with identity $(e_G,e_H)$, coordinatewise inverses, and homomorphic coordinate projections
- For every prime $p$, the two operations on $\mathbb{Z}/p$ make it a field
- For $n\ge 1$, every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$, so $\lvert\mathbb{Z}/n\rvert=n$; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$
- The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$, and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$
- A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$, and equality holds if and only if $B = A$
- The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$, and cyclic groups
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 96 results over 24 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
- Keith Conrad, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)