CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 \in {- 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.

[L1]

Such an operator satisfies $T^{- 1} = T^{*}$ and $T^{*} T = T T^{*} = I$ (For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and $T^{*} T = I$ are equivalent).

[L2]

Adjoints reverse products and fix the identity (Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ ).

[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 \geq 1$ the operator determinant is independent of the ordered basis, in dimension zero it is the separately defined value $1$ , and $\det (S \circ 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 (S T) = \det (S) \det (T)$ ).

[L5]

For $n \geq 1$ and $A \in M_{n} (R)$ over a commutative ring, $\det (A^{T}) = \det (A)$ ; complex conjugation is a field automorphism, and $z \overline{z} = ∣ z ∣^{2}$ (For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ , Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ 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.1

The identity satisfies [L1]. If $S, T$ satisfy it, then [L2] gives $(S T)^{*} (S T) = T^{*} S^{*} S T = 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.

L1L2

1.2

Suppose $\dim V = n \geq 1$ and choose an orthonormal basis by [L6]; write $A$ for the matrix of $T$ in it. By [L3] the matrix of $T^{*}$ is ${\overline{A}}^{T}$ , and since conjugation is a field automorphism it conjugates the determinant, so [L5] gives $\det ({\overline{A}}^{T}) = \det \overline{A} = \overline{\det A}$ . Hence [L4] makes $\det (T^{*}) = \overline{\det T}$ . Taking determinants in $T^{*} T = I$ , where $I$ has matrix $I_{n}$ and so determinant $1$ , [L4] gives $1 = \overline{\det T} \det T = ∣ \det T ∣^{2}$ , so [L5] yields $∣ \det T ∣ = 1$ .

L1L3L4L5L6choosealgebra

2.1

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.

step 1.2L4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 results over 18 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

Sheldon Axler, Linear Algebra Done Right, 4th ed., §7D (standard reference, not scraped)