# 2×2 determinants: the product rule, the scaling rule and the invertibility criterion over ℝ [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-determinant/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-determinant-01 · production-20261019-adopted-96 ## 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 S01 · definitionBefore M=\begin{pmatrix}a&b\\c&d\end{pmatrix} After \det(M)=ad-bc Conditions: none Rule: mko_det_def · Uses: G1 Leaf basis: mko_det_def + def_unfold State the MKO's definition: the product ad of the main diagonal minus the product bc of the other diagonal. Signs and positions matter: it may not be changed to ad+bc, nor may an absolute value be taken (MKO first paragraph). S02 · equivalentBefore \det(A),\ \det(B) After 2\cdot 3-1\cdot(-1)=7,\quad 1\cdot 0-(-2)\cdot 4=8 Conditions: none Rule: numeric_evaluation · Uses: S01, G2 Leaf basis: numeric_evaluation + neg_mul + mko_det_def det(A)=2·3−1·(−1)=6−(−1)=7: subtracting a negative product adds its opposite. det(B)=1·0−(−2)·4=0−(−8)=8. S03 · equivalentBefore A=\begin{pmatrix}a&b\\c&d\end{pmatrix},\ B=\begin{pmatrix}e&f\\g&h\end{pmatrix} After AB=\begin{pmatrix}ae+bg&af+bh\\ce+dg&cf+dh\end{pmatrix} Conditions: none Rule: matrix_product_def · Uses: G1, matrix_product_def Leaf basis: matrix_product_def + def_unfold By the definition of the matrix product, (AB)(i,j)=Σ_{k=1}^{2}A(i,k)B(k,j): the sum of products of row i with column j. For example (AB)(1,1)=ae+bg and (AB)(2,2)=cf+dh. S04 · equivalentBefore \det(AB)=(ae+bg)(cf+dh)-(af+bh)(ce+dg) After \det(AB)=(ad-bc)(eh-fg)=\det(A)\det(B) Conditions: none Rule: L_det_mul · Uses: S01, S03, L_det_mul Leaf basis: L_det_mul + mko_det_def Applying the definition of S01 to AB from S03 gives the left side. By Lemma L_det_mul it equals det(A)det(B). The lemma is proved in S04.1 to S04.4 by expanding and comparing monomials, for all reals a through h, so it holds for all 2×2 real matrices. S05 · impliesBefore AB After AB=\begin{pmatrix}6&-4\\11&2\end{pmatrix},\ \det(AB)=12+44=56=7\cdot 8 Conditions: none Rule: numeric_evaluation · Uses: S02, S03, S04, G2 Leaf basis: numeric_evaluation + matrix_product_def + mko_det_def Compute directly by S03: (AB)(1,1)=2·1+1·4=6, (AB)(1,2)=2·(−2)+1·0=−4, (AB)(2,1)=(−1)·1+3·4=11, (AB)(2,2)=(−1)(−2)+3·0=2. det(AB)=6·2−(−4)·11=12+44=56, the same as det(A)det(B)=7·8=56. This is a check by recomputing from the actual product (MKO third paragraph). S06 · impliesBefore BA After BA=\begin{pmatrix}4&-5\\8&4\end{pmatrix}\neq AB,\ \det(BA)=16+40=56 Conditions: none Rule: matrix_product_def · Uses: S03, S05, G2 Leaf basis: matrix_product_def + numeric_evaluation BA: (1,1)=1·2+(−2)(−1)=4, (1,2)=1·1+(−2)·3=−5, (2,1)=4·2+0·(−1)=8, (2,2)=4·1+0·3=4. The top-left entries 4≠6, so BA≠AB; yet det(BA)=4·4−(−5)·8=56=det(AB). The product rule says only that the determinants agree; it does not say that A and B commute (MKO assumption a3). S07 · equivalentBefore \det(tM),\ tM=\begin{pmatrix}ta&tb\\tc&td\end{pmatrix} After (ta)(td)-(tb)(tc)=t^2(ad-bc)=t^2\det(M) Conditions: none Rule: distributive · Uses: S01, matrix_alg Leaf basis: mul_comm + mul_assoc + distributive + power_laws Every entry of tM is multiplied by t. By definition det(tM)=(ta)(td)−(tb)(tc); by commutativity and associativity of multiplication, (ta)(td)=t²ad and (tb)(tc)=t²bc; distributivity then factors out t². Each product contains two entries, which is why t² appears and not t. S08 · impliesBefore -3A=\begin{pmatrix}-6&-3\\3&-9\end{pmatrix} After \det(-3A)=54+9=63=(-3)^2\cdot 7;\ \det(0A)=0 Conditions: none Rule: numeric_evaluation · Uses: S02, S07, G2 Leaf basis: numeric_evaluation + mko_det_def Directly: det(−3A)=(−6)(−9)−(−3)·3=54+9=63; by S07 it should be (−3)²·7=9·7=63, which agrees. A negative t acts through t², so the determinant does not change sign (MKO assumption a2). For t=0, 0A is the zero matrix, with determinant 0=0²·7. S09 · equivalentBefore M\,\operatorname{adj}(M),\ \operatorname{adj}(M)\,M,\ \operatorname{adj}(M)=\begin{pmatrix}d&-b\\-c&a\end{pmatrix} After \begin{pmatrix}ad-bc&0\\0&ad-bc\end{pmatrix}=\det(M)\,I Conditions: none Rule: matrix_product_def · Uses: S01, matrix_product_def Leaf basis: matrix_product_def + neg_mul + mul_comm + add_inverse The four entries of M·adj(M): (1,1)=ad+b(−c)=ad−bc, (1,2)=a(−b)+ba=0, (2,1)=cd+d(−c)=0, (2,2)=c(−b)+da=ad−bc. For adj(M)·M: (1,1)=da+(−b)c=ad−bc, (1,2)=db+(−b)d=0, (2,1)=(−c)a+ac=0, (2,2)=(−c)b+ad=ad−bc. Both products equal det(M)·I. S10 · impliesBefore \det(M)\neq 0 After X=\tfrac{1}{\det(M)}\operatorname{adj}(M):\ MX=XM=I Conditions: \det(M)\neq 0 Rule: mul_inverse_nonzero · Uses: S09, matrix_alg, mul_inverse_nonzero, G3 Leaf basis: mul_inverse_nonzero + matrix_alg + frac_rules If det(M)≠0, then 1/det(M) exists. Let X=(1/det(M))·adj(M). Since scalars factor out (matrix_alg), MX=(1/det(M))·(M·adj(M))=(1/det(M))·det(M)·I=I, and likewise XM=I. So M is invertible over ℝ. S11 · impliesBefore MX=XM=I After \det(M)\det(X)=\det(I)=1\ \Rightarrow\ \det(M)\neq 0 Conditions: none Rule: contradiction · Uses: S04, matrix_alg, G3 Leaf basis: L_det_mul + mul_zero + contradiction + numeric_evaluation Suppose M is invertible over ℝ with MX=I. By L_det_mul, det(M)det(X)=det(MX)=det(I)=1·1−0·0=1. If det(M)=0, the left side would be 0·det(X)=0, giving 0=1, a contradiction. So det(M)≠0. S12 · impliesBefore \det(M)\neq 0\Rightarrow\text{invertible},\ \text{invertible}\Rightarrow\det(M)\neq 0 After M\ \text{invertible over }\mathbb{R}\iff\det(M)\neq 0;\ \det(D)=2\cdot 2-4\cdot 1=0 Conditions: none Rule: iff_intro · Uses: S10, S11, G2 Leaf basis: iff_intro + numeric_evaluation The two directions S10 and S11 give the invertibility criterion over ℝ. For example D=[[2,4],[1,2]] has determinant 2·2−4·1=0, so D is not invertible over ℝ; indeed D(2,−1)ᵀ=(0,0)ᵀ sends a nonzero vector to zero, which cannot be undone. S13 · impliesBefore A^{-1} After 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 Conditions: \det(A)=7\neq 0 Rule: mul_inverse_nonzero · Uses: S02, S09, S10, G2 Leaf basis: mul_inverse_nonzero + matrix_product_def + numeric_evaluation det(A)=7≠0, so by S10 A⁻¹=(1/7)adj(A) with adj(A)=[[3,−1],[1,2]]. Check A·adj(A) directly: (1,1)=2·3+1·1=7, (1,2)=2·(−1)+1·2=0, (2,1)=(−1)·3+3·1=0, (2,2)=(−1)(−1)+3·2=7, so after multiplying by 1/7 it is I. The entries 3/7, −1/7, 1/7, 2/7 of A⁻¹ are not integers. S14 · impliesBefore AY=YA=I,\ Y\ \text{with integer entries}\ ? After Y=A^{-1}\ \text{and}\ \tfrac{3}{7}\notin\mathbb{Z}\ \Rightarrow\ \text{no integer inverse} Conditions: none Rule: contradiction · Uses: S13, matrix_alg, G3 Leaf basis: matrix_alg + contradiction + divides_def The inverse is unique: if X=A⁻¹ and Y also satisfies AY=YA=I, then by associativity (matrix_alg) X=XI=X(AY)=(XA)Y=IY=Y. So every inverse equals A⁻¹, whose (1,1) entry is 3/7, not an integer (7 does not divide 3). Hence A has no integer inverse, although its entries are integers and det(A)=7≠0. The real-field rule 'nonzero means invertible' does not carry over unchanged to the integer ring (MKO assumption a1). S15 · impliesBefore C=\begin{pmatrix}1&2\\3&4\end{pmatrix} After \det(C)=-2\neq 0,\ C^{-1}=\begin{pmatrix}-2&1\\ \tfrac{3}{2}&-\tfrac{1}{2}\end{pmatrix} Conditions: none Rule: iff_intro · Uses: S10, S12, G2 Leaf basis: iff_intro + mul_inverse_nonzero + numeric_evaluation det(C)=1·4−2·3=−2, negative but nonzero, so by S12 C is invertible; by S10, C⁻¹=(1/(−2))·[[4,−2],[−3,1]]=[[−2,1],[3/2,−1/2]]. Check C·C⁻¹: (1,1)=1·(−2)+2·(3/2)=1, (1,2)=1·1+2·(−1/2)=0, (2,1)=3·(−2)+4·(3/2)=0, (2,2)=3·1+4·(−1/2)=1. Nonzero determinants include positive and negative values and need not equal one (MKO first paragraph). S16 · impliesBefore \text{tasks of the goal} After \det(AB)=\det A\det B,\ \det(tM)=t^2\det M,\ \text{invertible over }\mathbb{R}\iff\det\neq 0 Conditions: none Rule: and_intro_elim · Uses: S04, S05, S06, S07, S08, S12, S13, S14, S15 Leaf basis: and_intro_elim Combine: the product and scaling rules hold for all 2×2 real matrices (S04, S07); in the example det(AB)=det(BA)=56 but AB≠BA (S05, S06), and det(−3A)=63 (S08); invertible over ℝ ⇔ det≠0 (S12); A⁻¹=(1/7)[[3,−1],[1,2]] is not an integer matrix (S13, S14); C with det(C)=−2 is invertible (S15). ## Substeps and lemmas S04.1 · equivalentBefore (ae+bg)(cf+dh) After acef+adeh+bcfg+bdgh Conditions: none Rule: distributive · Uses: distributive, mul_comm, mul_assoc Leaf basis: distributive + mul_comm + mul_assoc Expand by distributivity into four products: ae·cf, ae·dh, bg·cf, bg·dh; then use commutativity and associativity of multiplication to put the letters of each monomial in alphabetical order: acef, adeh, bcfg, bdgh. S04.2 · equivalentBefore (af+bh)(ce+dg) After acef+adfg+bceh+bdgh Conditions: none Rule: distributive · Uses: distributive, mul_comm, mul_assoc Leaf basis: distributive + mul_comm + mul_assoc Expand the same way: af·ce=acef, af·dg=adfg, bh·ce=bceh, bh·dg=bdgh. S04.3 · equivalentBefore (acef+adeh+bcfg+bdgh)-(acef+adfg+bceh+bdgh) After adeh+bcfg-adfg-bceh Conditions: none Rule: add_inverse · Uses: S04.1, S04.2 Leaf basis: add_inverse + add_comm + add_assoc + distributive On subtraction, acef and bdgh appear in both expansions and cancel (u−u=0); what remains is adeh+bcfg−adfg−bceh. S04.4 · equivalentBefore (ad-bc)(eh-fg) After adeh-adfg-bceh+bcfg Conditions: none Rule: distributive · Uses: S04.3, distributive Leaf basis: distributive + neg_mul + mul_comm + mul_assoc Expand the right side: ad·eh=adeh, ad·(−fg)=−adfg, (−bc)·eh=−bceh and (−bc)(−fg)=bcfg (neg_mul). These are term for term the four terms of S04.3, so det(AB)=det(A)det(B). S04.1 to S04.4 together prove Lemma L_det_mul. ## 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 positiveOne 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 productThe 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 systemOver ℝ, 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-determinant-01.json)