Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13
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 A,B∈Mn(F), the products AB and BA have the same characteristic polynomial

Statement

For A,B∈Mn(F),

χAB(x)=χBA(x).

Facts & Assumptions

Given: Matrices A,B∈Mn(F).

[L2]

For a positive-sized square matrix over a commutative ring, the determinant is the signed sum over permutations of products selecting one entry in each row and column (For n≥1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣ for a real matrix).

[L3]

Determinants are multiplicative for positive-sized square matrices over a commutative ring (For same-sized finite square matrices over a commutative ring, det⁡(AB)=det⁡(A)det⁡(B)).

[L4]

Block multiplication follows from associative and distributive matrix arithmetic (Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products).

Proof

technique · direct
1.1

If n=0, both characteristic polynomials are 1 by [L1]. Assume henceforth that n≥1, and work over F[t].

L1
1.2

Put N=(ItA−BI). Left multiplication by (I−tA0I) produces (I+tAB0−BI), while left multiplication by (I0BI) produces (ItA0I+tBA).

L4algebra
2.1

In the Leibniz sum [L2] for a block-triangular matrix, every nonzero term preserves the two index blocks, so its determinant is the product of the two diagonal-block determinants. Both multiplying matrices in step 1.2 consequently have determinant 1, and [L3] yields det⁡(I+tAB)=det⁡(N)=det⁡(I+tBA) in F[t].

step 1.2L2L3algebra
3.1

Replacing t by −t, the coefficient of tk in det⁡(I−tC) is the coefficient of xn−k in det⁡(xI−C), directly from the Leibniz formula. Equality in step 2.1 therefore gives equality of every coefficient of χAB and χBA.

step 2.1L1L2algebra
4.1

Together with the zero-sized case, χAB=χBA for all n.

step 1.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources