Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16
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.

Orthogonal and unitary operators form groups, and their determinants have modulus one

Statement

The orthogonal operators on a finite-dimensional real inner product space form a group under composition, as do the unitary operators on a finite-dimensional complex inner product space. Every such operator T satisfies

∣det⁡T∣=1.

Over R, this says det⁡T∈{−1,1}. In dimension zero, the unique determinant is 1.

Facts & Assumptions

Given: Orthogonal or unitary operators on a fixed finite-dimensional inner product space.

[L3]

In an orthonormal basis, the matrix of T∗ is the conjugate transpose of the matrix of T (In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix).

[L4]

For dim⁡V≥1 the operator determinant is independent of the ordered basis, in dimension zero it is the separately defined value 1, and det⁡(S∘T)=det⁡(S)det⁡(T) (The determinant of a linear operator is independent of the chosen ordered basis, For endomorphisms S and T of one finite-dimensional vector space, det⁡(ST)=det⁡(S)det⁡(T)).

[L5]

For n≥1 and A∈Mn(R) over a commutative ring, det⁡(AT)=det⁡(A); complex conjugation is a field automorphism, and zz‾=∣z∣2 (For every square matrix over a commutative ring, det⁡(AT)=det⁡(A), Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L6]

Every finite-dimensional real or complex inner product space has an orthonormal basis, the empty one in dimension zero (Every finite-dimensional real or complex inner product space has an orthonormal basis).

Proof

technique · direct
1.1L1L2

The identity satisfies [L1]. If S,T satisfy it, then [L2] gives (ST)∗(ST)=T∗S∗ST=I; and the inverse T−1=T∗ also satisfies the same identities. Hence the operators are closed under identity, composition, and inverses, so form a group.

1.2L1L3L4L5L6choosealgebra

Suppose dim⁡V=n≥1 and choose an orthonormal basis by [L6]; write A for the matrix of T in it. By [L3] the matrix of T∗ is A‾T, and since conjugation is a field automorphism it conjugates the determinant, so [L5] gives det⁡(A‾T)=det⁡A‾=det⁡A‾. Hence [L4] makes det⁡(T∗)=det⁡T‾. Taking determinants in T∗T=I, where I has matrix In and so determinant 1, [L4] gives 1=det⁡T‾det⁡T=∣det⁡T∣2, so [L5] yields ∣det⁡T∣=1.

2.1step 1.2L4∎

Over R, the only real scalars of modulus one are −1 and 1. If V=0, then [L4] gives the operator determinant 1, so ∣det⁡T∣=1 holds there as well, and the group has its single identity element.

Depends on

Used by

Dependency tree · two levels

33 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