Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

If AA is invertible over a commutative ring, then det⁡(A−1)=det⁡(A)−1\det(A^{-1})=\det(A)^{-1}

Statement

Let n≥1n\ge1. If A∈Mn(R)A\in M_n(R) is invertible over a commutative ring, then det⁡(A−1)=det⁡(A)−1.\det(A^{-1})=\det(A)^{-1}.

Facts & Assumptions

Given: An invertible matrix AA over a commutative ring.

[L1]

det⁡(A)\det(A) is a unit (An invertible square matrix over a commutative ring has unit determinant).

[L2]

det⁡(AA−1)=det⁡(A)det⁡(A−1)\det(AA^{-1})=\det(A)\det(A^{-1}) (For same-sized finite square matrices over a commutative ring, det⁡(AB)=det⁡(A)det⁡(B)\det(AB)=\det(A)\det(B)).

[L3]

The inverse of a unit is unique (The units of a ring are the invertible elements of its multiplicative monoid, and R×R^{\times} is a group under multiplication; 0∈R×0 \in R^{\times} only in the zero ring).

[L4]

Matrix invertibility gives AA−1=InAA^{-1}=I_n (Invertible square matrices and similarity over a commutative ring).

[L5]

The determinant is normalized: det⁡(In)=1\det(I_n)=1 (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

Proof

technique · direct
1.1

By [L2], [L4] and [L5], det⁡(A)det⁡(A−1)=det⁡(In)=1\det(A)\det(A^{-1})=\det(I_n)=1, so det⁡(A−1)\det(A^{-1}) is an inverse of the unit det⁡(A)\det(A).

L1L2L3L4L5
2.1

Uniqueness of the inverse in [L3] gives det⁡(A−1)=det⁡(A)−1\det(A^{-1})=\det(A)^{-1}.

step 1.1L3∎

Depends on

Used by

Dependency tree · next 3 levels

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