2×2 determinants: the product rule, the scaling rule and the invertibility criterion over ℝ

Goal and scope

For all 2×2 real matrices prove det(AB)=det(A)det(B) and det(tM)=t²det(M), and prove that M is invertible over ℝ exactly when det(M)≠0. With A=[[2,1],[−1,3]] and B=[[1,−2],[4,0]], check the product rule and show AB≠BA; check the scaling rule with t=−3; find A⁻¹ and explain why A, although an integer matrix with det(A)=7≠0, has no integer inverse; use C=[[1,2],[3,4]] (det=−2) to show that a nonzero determinant need not be positive.

Stays inside the MKO's scope: 2×2 square matrices, the real field, the usual row-by-column matrix product. It fully proves the product rule, the scaling rule and the invertibility criterion over ℝ; it does not treat higher-order determinants or invertibility criteria over general rings, and does not build the Lean det_fin_two bridge; it does not change the canonical MKO or its English edition.

Givens and symbols

• distributive
• mul_comm
• mul_assoc
• matrix_product_def
• mul_inverse_nonzero
• numeric_evaluation

• G1 — All matrices are 2×2 real matrices over the field ℝ; AB is the usual row-by-column product, not the entrywise product (MKO assumptions a1, a3).
• G2 — Examples: A=[[2,1],[−1,3]], B=[[1,−2],[4,0]], t=−3, C=[[1,2],[3,4]], D=[[2,4],[1,2]] (each inner bracket is a row).
• G3 — M is invertible over ℝ if there is a real matrix X with MX=XM=I; an 'integer inverse' is such an X whose entries are all integers.

• \det(M) — the determinant ad−bc of a 2×2 matrix M=[[a,b],[c,d]]
• AB — the row-by-column matrix product
• tM — the scalar multiple of M by t
• \operatorname{adj}(M) — the adjugate [[d,−b],[−c,a]]
• I — the 2×2 identity matrix

Rules and sources

• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_det_def · cited — For M=[[a,b],[c,d]] over R, define D(M)=det(M)=ad−bc. M is invertible over R exactly when det(M)≠0. For 2×2 real matrices A,B, det(AB)=det(A)det(B), and det(tM)=t²det(M). · mko-determinant
• matrix_alg · prerequisite — Multiplication of 2×2 matrices is associative: (XY)Z=X(YZ); I=[[1,0],[0,1]] satisfies IX=XI=X; scalars factor out: X(kY)=(kX)Y=k(XY); tM multiplies every entry by t.
• L_det_mul · lemma — For all 2×2 real matrices A and B: det(AB)=det(A)det(B).

Main derivation

M=\begin{pmatrix}a&b\\c&d\end{pmatrix}

\det(M)=ad-bc

\det(A),\ \det(B)

2\cdot 3-1\cdot(-1)=7,\quad 1\cdot 0-(-2)\cdot 4=8

A=\begin{pmatrix}a&b\\c&d\end{pmatrix},\ B=\begin{pmatrix}e&f\\g&h\end{pmatrix}

AB=\begin{pmatrix}ae+bg&af+bh\\ce+dg&cf+dh\end{pmatrix}

\det(AB)=(ae+bg)(cf+dh)-(af+bh)(ce+dg)

\det(AB)=(ad-bc)(eh-fg)=\det(A)\det(B)

AB

AB=\begin{pmatrix}6&-4\\11&2\end{pmatrix},\ \det(AB)=12+44=56=7\cdot 8

BA

BA=\begin{pmatrix}4&-5\\8&4\end{pmatrix}\neq AB,\ \det(BA)=16+40=56

\det(tM),\ tM=\begin{pmatrix}ta&tb\\tc&td\end{pmatrix}

(ta)(td)-(tb)(tc)=t^2(ad-bc)=t^2\det(M)

-3A=\begin{pmatrix}-6&-3\\3&-9\end{pmatrix}

\det(-3A)=54+9=63=(-3)^2\cdot 7;\ \det(0A)=0

M\,\operatorname{adj}(M),\ \operatorname{adj}(M)\,M,\ \operatorname{adj}(M)=\begin{pmatrix}d&-b\\-c&a\end{pmatrix}

\begin{pmatrix}ad-bc&0\\0&ad-bc\end{pmatrix}=\det(M)\,I

\det(M)\neq 0

X=\tfrac{1}{\det(M)}\operatorname{adj}(M):\ MX=XM=I

MX=XM=I

\det(M)\det(X)=\det(I)=1\ \Rightarrow\ \det(M)\neq 0

\det(M)\neq 0\Rightarrow\text{invertible},\ \text{invertible}\Rightarrow\det(M)\neq 0

M\ \text{invertible over }\mathbb{R}\iff\det(M)\neq 0;\ \det(D)=2\cdot 2-4\cdot 1=0

A^{-1}

A^{-1}=\tfrac{1}{7}\begin{pmatrix}3&-1\\1&2\end{pmatrix},\ A\cdot\tfrac{1}{7}\begin{pmatrix}3&-1\\1&2\end{pmatrix}=\tfrac{1}{7}\begin{pmatrix}7&0\\0&7\end{pmatrix}=I

AY=YA=I,\ Y\ \text{with integer entries}\ ?

Y=A^{-1}\ \text{and}\ \tfrac{3}{7}\notin\mathbb{Z}\ \Rightarrow\ \text{no integer inverse}

C=\begin{pmatrix}1&2\\3&4\end{pmatrix}

\det(C)=-2\neq 0,\ C^{-1}=\begin{pmatrix}-2&1\\ \tfrac{3}{2}&-\tfrac{1}{2}\end{pmatrix}

\text{tasks of the goal}

\det(AB)=\det A\det B,\ \det(tM)=t^2\det M,\ \text{invertible over }\mathbb{R}\iff\det\neq 0

Substeps and lemmas

(ae+bg)(cf+dh)

acef+adeh+bcfg+bdgh

(af+bh)(ce+dg)

acef+adfg+bceh+bdgh

(acef+adeh+bcfg+bdgh)-(acef+adfg+bceh+bdgh)

adeh+bcfg-adfg-bceh

(ad-bc)(eh-fg)

adeh-adfg-bceh+bcfg

Reverse audits

• S16 · sufficient_goal_reduction · S04, S05, S06, S07, S08, S12, S13, S14, S15 — Goal G: the items asked for. Sufficient condition H: the conclusions of S04 to S15; H⇒G uses only conjunction. H is derived forwards from G1 to G3; G is never used as a premise.
• S15 · premise_audit · S12, numeric_evaluation — It relies on the criterion and the numeric checks (N24 to N28).
• S14 · premise_audit · S13, matrix_alg, contradiction, divides_def — It needs uniqueness of the inverse (associativity) and that 3/7 is not an integer; no general invertibility criterion over the integers is claimed.
• S13 · premise_audit · S10, numeric_evaluation — The numeric check (N20 to N23) confirms A·A⁻¹=I; A⁻¹·A=I is guaranteed by the general argument of S09 and S10.
• S12 · premise_audit · S10, S11, iff_intro — Each direction has its own proof; the example D only illustrates and is not part of the proof.
• S11 · premise_audit · L_det_mul, mul_zero, contradiction — This is the direction 'invertible ⇒ det≠0', using only the product rule and det(I)=1.
• S10 · premise_audit · S09, mul_inverse_nonzero, matrix_alg — The key is dividing by det(M), which needs det(M)≠0 and a number system with division, such as ℝ; this is the direction 'det≠0 ⇒ invertible'.
• S09 · inverse_equivalence · matrix_product_def, neg_mul, mul_comm — Every entry is an identity (N18, N19), so it is two-way.
• S08 · premise_audit · S07, numeric_evaluation — The two methods (direct and by the formula) agree (N16, N17); this checks the example only.
• S07 · inverse_equivalence · mul_comm, mul_assoc, distributive — An identity for all reals t, a, b, c, d (N15), two-way.
• S06 · premise_audit · matrix_product_def, numeric_evaluation — One unequal entry suffices for BA≠AB.
• S05 · premise_audit · S03, S04, numeric_evaluation — The finite computation checks this example only (N3 to N8) and does not replace the general proof of S04.
• S04.4 · inverse_equivalence · distributive, neg_mul, mul_comm — Identities, two-way; N14 checks the same polynomial identity on a grid.
• S04.3 · inverse_equivalence · add_inverse, add_comm, add_assoc — Additive inverses and rearrangement are identities, so it is two-way.
• S04.2 · inverse_equivalence · distributive, mul_comm, mul_assoc — Identities, two-way.
• S04.1 · inverse_equivalence · distributive, mul_comm, mul_assoc — Only identities are used, so it is two-way.
• S04 · inverse_equivalence · L_det_mul, eq_refl_symm_trans — The two sides form a polynomial identity valid for all reals (N14), so the equality is two-way.
• S03 · inverse_equivalence · matrix_product_def — This unfolds the definition at all four positions, two-way.
• S02 · inverse_equivalence · numeric_evaluation, neg_mul — Exact integer computation (N1, N2), two-way.
• S01 · premise_audit · G1, mko_det_def — This step only states the definition; it derives no new fact.

Error controls and negative controls

Nonzero need not be positive

One misconception the MKO names is that invertibility needs a positive determinant. det(C)=−2<0, yet C is invertible, with the inverse written out in S15. The criterion is det≠0, not det>0 and not det=1.

AB is not the entrywise product

The entrywise product of A and B is [[2,−2],[−4,0]], with determinant 2·0−(−2)(−4)=−8, not 56. The product rule holds for the row-by-column product AB only, and it does not mean AB=BA (S06).

The criterion depends on the number system

Over ℝ, det(A)=7≠0 is enough for invertibility; but the entries of A⁻¹ are fractions such as 3/7, and the inverse is unique, so A has no integer inverse (S14). Ignoring the number system is a misconception the MKO lists.

• det(C)=−2<0, so C is not invertible → reject — The criterion is det≠0; C⁻¹=[[−2,1],[3/2,−1/2]] exists.
• The entrywise product [[2,−2],[−4,0]] has determinant det(A)det(B) → reject — Its determinant is −8, whereas det(A)det(B)=56.
• det(AB)=det(BA), so AB=BA → reject — The top-left entry of AB is 6 and that of BA is 4.
• det(−3A)=−3·det(A)=−21 → reject — For 2×2 matrices det(tM)=t²det(M), so it is 9·7=63.
• A has integer entries and det(A)=7≠0, so A has an integer inverse → reject — The unique inverse (1/7)[[3,−1],[1,2]] contains the non-integer 3/7.

Result and limitations

For all 2×2 real matrices, det(AB)=det(A)det(B) and det(tM)=t²det(M), and M is invertible over ℝ exactly when det(M)≠0. In the example det(A)=7, det(B)=8, det(AB)=det(BA)=56 while AB≠BA; det(−3A)=63; A⁻¹=(1/7)[[3,−1],[1,2]], and A has no integer inverse; det(C)=−2 and C is invertible.

• This guide treats 2×2 matrices only; higher-order determinants and the general invertibility criterion over the integers are out of scope.
• matrix_alg (associativity of matrix multiplication, the identity matrix, factoring out scalars) is used as a prerequisite and is not proved entry by entry here.
• The MKO's formal next step (bridging det_fin_two, det_mul, det_smul and the real-field inverse) is not done.

Verification and source binding

32 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: a1bb7c2c935079e026c6f8947b4a0da75f8f3294086082e985d4bf8fb3003bb9
• original source SHA-256: a1bb7c2c935079e026c6f8947b4a0da75f8f3294086082e985d4bf8fb3003bb9
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)