Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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 p, Aut((Z/p)×(Z/p))=(p21)(p2p)

Statement

For every prime p, Aut((Z/p)×(Z/p))=(p21)(p2p). See Group isomorphisms, automorphisms and the set Aut(G).

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

An isomorphism is a bijective group homomorphism; an automorphism is an isomorphism from a group to itself, and Aut(G):={f:GG:f is an automorphism}. (Group isomorphisms, automorphisms and the set Aut(G)).

[L2]

Let G and H be groups. Their external direct product has underlying set G×H:={(g,h):gG, hH} and componentwise operation (g,h)(g,h):=(gg,hh). The fact that this operation makes G×H 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 G×H with componentwise multiplication).

[L3]

For groups G and H, the componentwise operation of def-external-direct-product-of-groups makes G×H a group. Its identity is (eG,eH), and (g,h)1=(g1,h1). Moreover the coordinate maps πG(g,h)=g and πH(g,h)=h are group homomorphisms. (G×H is a group with identity (eG,eH), coordinatewise inverses, and homomorphic coordinate projections).

[L4]

For every prime p, the operations of addition and multiplication on Z/p make it a field (def-field). (For every prime p, the two operations on Z/p make it a field).

[L5]

Let n be a positive integer. Every class in Z/n (def-integers-modulo-n) contains exactly one integer r with 0r<n. Consequently the map r[r]n(0r<n) is a bijection from the von Neumann natural n to Z/n, and Z/n=n. This includes n=1, where the only representative is 0. For n=0, the map a[a]0 is a bijection ZZ/0. (For n1, every class in Z/n has one representative r with 0r<n, so Z/n=n; while Z/0 is in bijection with Z).

[L6]
  1. If A and B are finite then A×B is finite and A×B=AB (def-finite-cardinality). 2. Let mN and let A0,,Am1 be finite sets. Write i<mAi:={f:f is a function with domain m and f(i)Ai for every i<m}. Then i<mAi is finite and i<mAi=i<mAi, the right-hand product being the N-valued one of def-nat-finite-sum-and-product. (The product rule: A×B=AB, and i<mAi=i<mAi).
[L7]

Let A be a finite set (def-countable) and let BA. Then: 1. B is finite; 2. BA (def-finite-cardinality); 3. B=A if and only if B=A; 4. every injection f:AA is a bijection, and every surjection f:AA is a bijection. (A subset of a finite set is finite, with BA, and equality holds if and only if B=A).

[L8]

For a subset S of a group G, the generated subgroup is S:={H:HG and SH}, the smallest subgroup of G containing S. (The subgroup S generated by a subset, the cyclic subgroup g, and cyclic groups).

Proof

technique · direct
1.1

In the additive group Ep=(Z/p)×(Z/p), a homomorphism EpEp is determined by the images u and v of the two coordinate generators, because every element has a unique coordinate expression.

L1L2L3L4L5L6L7L8givenalgebra
2.1

If u=0 or vu, the image is a proper cyclic subgroup. If u0 and vu, the p elements of each coset jv+u are disjoint as j varies, so u,v generate all p2 elements and the homomorphism is bijective.

step 1.1givenalgebra
3.1

There are p21 choices for nonzero u. Its cyclic subgroup has exactly p elements, leaving p2p choices for v; multiplication gives (p21)(p2p) automorphisms.

step 2.1givenalgebra
4.1

When p=2, the same count gives (41)(42)=6; the argument is entirely in coordinates and makes no matrix-group identification. This proves the stated claim.

step 1.1step 2.1step 3.1givenalgebra

Depends on

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