Grace/Cumulus/Algebra/Ring/DeterminantThree.g17

Open in Workbench Download source

Imports

PermutationSign · DeterminantIdentity · Combinatorics.Permutations

Declarations

Source

1-- The determinant of a 3 × 3 matrix over a commutative ring as the2-- six-term Leibniz formula: the six permutations of 3 listed with their3-- signs, a finite sum over six listed points, and the expansion4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Ring.DeterminantThree10import PermutationSign11import DeterminantIdentity12import Combinatorics.Permutations1314-- Peeling one point off the sum of a function restricted to a finite set.15theorem finiteRingSum.insert_restrict (V A add zero neg mul one f D a : Set)16  requires ring : IsCommRing(A, add, zero, neg, mul, one)17  requires finite : Finite(V)18  requires function : f : D → A19  requires subset : insert(a, V) ⊆ D20  requires fresh : ¬(a ∈ V)21  shows finiteRingSum(insert(a, V), A, add, zero, neg, mul, one,22      restrict(f, insert(a, V))) =23    call2(add, finiteRingSum(V, A, add, zero, neg, mul, one, restrict(f, V)),24      f(a))25proof26  have weights := restrict.domain_function at f, D, A, insert(a, V)27    with function, subset28  have step := finiteRingSum.insert at V, A, add, zero, neg, mul, one,29    restrict(f, insert(a, V)), a with ring, finite, weights, fresh30  have inner : V ⊆ insert(a, V)31    intros x hx32    exact insert.contains with hx33  have nested := restrict.nested at f, V, insert(a, V) with inner34  have self := insert.self at a, V35  have value := restrict.domain_apply at f, D, A, insert(a, V), a36    with function, subset, self37  rw [step, nested, value]38  rfl3940-- The sum of a function over six listed points.41theorem finiteRingSum.six (A add zero neg mul one f D p q r s t u : Set)42  requires ring : IsCommRing(A, add, zero, neg, mul, one)43  requires function : f : D → A44  requires subset : insert(u, insert(t, insert(s, insert(r, insert(q, {p}))))) ⊆ D45  requires freshQ : ¬(q ∈ {p})46  requires freshR : ¬(r ∈ insert(q, {p}))47  requires freshS : ¬(s ∈ insert(r, insert(q, {p})))48  requires freshT : ¬(t ∈ insert(s, insert(r, insert(q, {p}))))49  requires freshU : ¬(u ∈ insert(t, insert(s, insert(r, insert(q, {p})))))50  shows finiteRingSum(insert(u, insert(t, insert(s, insert(r, insert(q, {p}))))),51      A, add, zero, neg, mul, one,52      restrict(f, insert(u, insert(t, insert(s, insert(r, insert(q, {p}))))))) =53    call2(add, call2(add, call2(add, call2(add, call2(add, f(p), f(q)), f(r)),54      f(s)), f(t)), f(u))55proof56  have finite1 := Finite.singleton at p57  have finite2 := Finite.insert at {p}, q with finite158  have finite3 := Finite.insert at insert(q, {p}), r with finite259  have finite4 := Finite.insert at insert(r, insert(q, {p})), s with finite360  have finite5 := Finite.insert at insert(s, insert(r, insert(q, {p}))), t61    with finite462  have sub5 : insert(t, insert(s, insert(r, insert(q, {p})))) ⊆ D63    intros x hx64    exact subset with x, (insert.contains with hx)65  have sub4 : insert(s, insert(r, insert(q, {p}))) ⊆ D66    intros x hx67    exact sub5 with x, (insert.contains with hx)68  have sub3 : insert(r, insert(q, {p})) ⊆ D69    intros x hx70    exact sub4 with x, (insert.contains with hx)71  have sub2 : insert(q, {p}) ⊆ D72    intros x hx73    exact sub3 with x, (insert.contains with hx)74  have sub1 : {p} ⊆ D75    intros x hx76    exact sub2 with x, (insert.contains with hx)77  have step6 := finiteRingSum.insert_restrict at78    insert(t, insert(s, insert(r, insert(q, {p})))), A, add, zero, neg, mul, one,79    f, D, u with ring, finite5, function, subset, freshU80  have step5 := finiteRingSum.insert_restrict at81    insert(s, insert(r, insert(q, {p}))), A, add, zero, neg, mul, one,82    f, D, t with ring, finite4, function, sub5, freshT83  have step4 := finiteRingSum.insert_restrict at84    insert(r, insert(q, {p})), A, add, zero, neg, mul, one,85    f, D, s with ring, finite3, function, sub4, freshS86  have step3 := finiteRingSum.insert_restrict at87    insert(q, {p}), A, add, zero, neg, mul, one,88    f, D, r with ring, finite2, function, sub3, freshR89  have step2 := finiteRingSum.insert_restrict at90    {p}, A, add, zero, neg, mul, one, f, D, q with ring, finite1, function, sub2, freshQ91  have weights1 := restrict.domain_function at f, D, A, {p} with function, sub192  have step1 := finiteRingSum.singleton at A, add, zero, neg, mul, one,93    restrict(f, {p}), p with ring, weights194  have selfP := singleton.self at p95  have valueP := restrict.domain_apply at f, D, A, {p}, p with function, sub1, selfP96  rw [step6, step5, step4, step3, step2, step1, valueP]97  rfl9899-- Two functions with different values at a point are different.100theorem apply.distinct (p q x a b : Set)101  requires hp : p(x) = a102  requires hq : q(x) = b103  requires different : a ≠ b104  shows p ≠ q105proof106  intro same107  rw [same, hq] at hp108  symm at hp109  exact different with hp110111-- The three indices and their distinctness.112theorem three.zero_mem113  shows 0 ∈ 3114proof115  typecheck116117theorem three.one_mem118  shows 1 ∈ 3119proof120  typecheck121122theorem three.two_mem123  shows 2 ∈ 3124proof125  typecheck126127theorem three.zero_ne_one128  shows 0 ≠ 1129proof130  intro equal131  arith132133theorem three.zero_ne_two134  shows 0 ≠ 2135proof136  intro equal137  arith138139theorem three.one_ne_two140  shows 1 ≠ 2141proof142  intro equal143  arith144145theorem three.one_ne_zero146  shows 1 ≠ 0147proof148  intro equal149  arith150151theorem three.two_ne_zero152  shows 2 ≠ 0153proof154  intro equal155  arith156157theorem three.two_ne_one158  shows 2 ≠ 1159proof160  intro equal161  arith162163-- The six permutations of 3: the identity, the three transpositions, and164-- the two three-cycles as composites of transpositions.165def swapZeroOne : Set := transposition(3, 0, 1)166def swapZeroTwo : Set := transposition(3, 0, 2)167def swapOneTwo : Set := transposition(3, 1, 2)168def cycleForward : Set := compose(swapZeroOne, swapOneTwo, 3, 3, 3)169def cycleBackward : Set := compose(swapZeroOne, swapZeroTwo, 3, 3, 3)170171theorem swapZeroOne.permutation172  shows swapZeroOne ∈ permutations(3)173proof174  unfold swapZeroOne175  exact permutations.transposition at 3, 0, 1 with three.zero_mem, three.one_mem176177theorem swapZeroTwo.permutation178  shows swapZeroTwo ∈ permutations(3)179proof180  unfold swapZeroTwo181  exact permutations.transposition at 3, 0, 2 with three.zero_mem, three.two_mem182183theorem swapOneTwo.permutation184  shows swapOneTwo ∈ permutations(3)185proof186  unfold swapOneTwo187  exact permutations.transposition at 3, 1, 2 with three.one_mem, three.two_mem188189theorem cycleForward.permutation190  shows cycleForward ∈ permutations(3)191proof192  unfold cycleForward193  exact permutations.compose at 3, swapOneTwo, swapZeroOne194    with swapOneTwo.permutation, swapZeroOne.permutation195196theorem cycleBackward.permutation197  shows cycleBackward ∈ permutations(3)198proof199  unfold cycleBackward200  exact permutations.compose at 3, swapZeroTwo, swapZeroOne201    with swapZeroTwo.permutation, swapZeroOne.permutation202203theorem swapZeroOne.values204  shows swapZeroOne(0) = 1 ∧ swapZeroOne(1) = 0 ∧ swapZeroOne(2) = 2205proof206  have first := transposition.first at 3, 0, 1 with three.zero_mem, three.one_mem207  have second := transposition.second at 3, 0, 1 with three.zero_mem, three.one_mem208  have other := transposition.other at 3, 0, 1, 2209    with three.zero_mem, three.one_mem, three.two_mem, three.two_ne_zero, three.two_ne_one210  unfold swapZeroOne211  exact ⟨first, second, other⟩212213theorem swapZeroTwo.values214  shows swapZeroTwo(0) = 2 ∧ swapZeroTwo(1) = 1 ∧ swapZeroTwo(2) = 0215proof216  have first := transposition.first at 3, 0, 2 with three.zero_mem, three.two_mem217  have second := transposition.second at 3, 0, 2 with three.zero_mem, three.two_mem218  have other := transposition.other at 3, 0, 2, 1219    with three.zero_mem, three.two_mem, three.one_mem, three.one_ne_zero, three.one_ne_two220  unfold swapZeroTwo221  exact ⟨first, other, second⟩222223theorem swapOneTwo.values224  shows swapOneTwo(0) = 0 ∧ swapOneTwo(1) = 2 ∧ swapOneTwo(2) = 1225proof226  have first := transposition.first at 3, 1, 2 with three.one_mem, three.two_mem227  have second := transposition.second at 3, 1, 2 with three.one_mem, three.two_mem228  have other := transposition.other at 3, 1, 2, 0229    with three.one_mem, three.two_mem, three.zero_mem, three.zero_ne_one, three.zero_ne_two230  unfold swapOneTwo231  exact ⟨other, first, second⟩232233theorem cycleForward.values234  shows cycleForward(0) = 1 ∧ cycleForward(1) = 2 ∧ cycleForward(2) = 0235proof236  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values237  obtain ⟨b0, b1, b2⟩ := swapOneTwo.values238  have outer := permutations.function with swapZeroOne.permutation239  have inner := permutations.function with swapOneTwo.permutation240  have at0 := compose.apply at swapZeroOne, swapOneTwo, 3, 3, 3, 0241    with inner, outer, three.zero_mem242  have at1 := compose.apply at swapZeroOne, swapOneTwo, 3, 3, 3, 1243    with inner, outer, three.one_mem244  have at2 := compose.apply at swapZeroOne, swapOneTwo, 3, 3, 3, 2245    with inner, outer, three.two_mem246  unfold cycleForward247  rw [at0, at1, at2, b0, b1, b2, a0, a1, a2]248  exact ⟨rfl, rfl, rfl⟩249250theorem cycleBackward.values251  shows cycleBackward(0) = 2 ∧ cycleBackward(1) = 0 ∧ cycleBackward(2) = 1252proof253  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values254  obtain ⟨b0, b1, b2⟩ := swapZeroTwo.values255  have outer := permutations.function with swapZeroOne.permutation256  have inner := permutations.function with swapZeroTwo.permutation257  have at0 := compose.apply at swapZeroOne, swapZeroTwo, 3, 3, 3, 0258    with inner, outer, three.zero_mem259  have at1 := compose.apply at swapZeroOne, swapZeroTwo, 3, 3, 3, 1260    with inner, outer, three.one_mem261  have at2 := compose.apply at swapZeroOne, swapZeroTwo, 3, 3, 3, 2262    with inner, outer, three.two_mem263  unfold cycleBackward264  rw [at0, at1, at2, b0, b1, b2, a0, a1, a2]265  exact ⟨rfl, rfl, rfl⟩266267theorem identity.three_values268  shows identity(3)(0) = 0 ∧ identity(3)(1) = 1 ∧ identity(3)(2) = 2269proof270  have at0 := identity.apply at 0, 3 with three.zero_mem271  have at1 := identity.apply at 1, 3 with three.one_mem272  have at2 := identity.apply at 2, 3 with three.two_mem273  exact ⟨at0, at1, at2⟩274275-- The six are pairwise distinct, each pair separated by a value.276theorem permutations.three_distinct277  shows swapZeroOne ≠ identity(3) ∧ swapZeroTwo ≠ identity(3) ∧278    swapOneTwo ≠ identity(3) ∧ cycleForward ≠ identity(3) ∧279    cycleBackward ≠ identity(3) ∧ swapZeroTwo ≠ swapZeroOne ∧280    swapOneTwo ≠ swapZeroOne ∧ cycleForward ≠ swapZeroOne ∧281    cycleBackward ≠ swapZeroOne ∧ swapOneTwo ≠ swapZeroTwo ∧282    cycleForward ≠ swapZeroTwo ∧ cycleBackward ≠ swapZeroTwo ∧283    cycleForward ≠ swapOneTwo ∧ cycleBackward ≠ swapOneTwo ∧284    cycleBackward ≠ cycleForward285proof286  obtain ⟨i0, i1, i2⟩ := identity.three_values287  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values288  obtain ⟨b0, b1, b2⟩ := swapZeroTwo.values289  obtain ⟨c0, c1, c2⟩ := swapOneTwo.values290  obtain ⟨f0, f1, f2⟩ := cycleForward.values291  obtain ⟨g0, g1, g2⟩ := cycleBackward.values292  have dAI := apply.distinct with a0, i0, three.one_ne_zero293  have dBI := apply.distinct with b0, i0, three.two_ne_zero294  have dCI := apply.distinct with c1, i1, three.two_ne_one295  have dFI := apply.distinct with f0, i0, three.one_ne_zero296  have dGI := apply.distinct with g0, i0, three.two_ne_zero297  have dBA := apply.distinct with b0, a0, three.two_ne_one298  have dCA := apply.distinct with c0, a0, three.zero_ne_one299  have dFA := apply.distinct with f1, a1, three.two_ne_zero300  have dGA := apply.distinct with g0, a0, three.two_ne_one301  have dCB := apply.distinct with c0, b0, three.zero_ne_two302  have dFB := apply.distinct with f0, b0, three.one_ne_two303  have dGB := apply.distinct with g1, b1, three.zero_ne_one304  have dFC := apply.distinct with f0, c0, three.one_ne_zero305  have dGC := apply.distinct with g0, c0, three.two_ne_zero306  have dGF := apply.distinct with g0, f0, three.two_ne_one307  exact ⟨dAI, dBI, dCI, dFI, dGI, dBA, dCA, dFA, dGA, dCB, dFB, dGB, dFC, dGC, dGF⟩308309-- Each of the six is new to the ones listed before it.310theorem permutations.three_fresh311  shows ¬(swapZeroOne ∈ {identity(3)}) ∧312    ¬(swapZeroTwo ∈ insert(swapZeroOne, {identity(3)})) ∧313    ¬(swapOneTwo ∈ insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))) ∧314    ¬(cycleForward ∈ insert(swapOneTwo, insert(swapZeroTwo,315      insert(swapZeroOne, {identity(3)})))) ∧316    ¬(cycleBackward ∈ insert(cycleForward, insert(swapOneTwo,317      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))318proof319  obtain ⟨dAI, dBI, dCI, dFI, dGI, dBA, dCA, dFA, dGA, dCB, dFB, dGB, dFC, dGC, dGF⟩ :=320    permutations.three_distinct321  constructor322  . intro member323    have equal := singleton.membership.forward with member324    exact dAI with equal325  constructor326  . intro member327    have alternatives0 := insert.membership.forward with member328    rcases alternatives0 with equal0 | rest0329    . exact dBA with equal0330    . have equal := singleton.membership.forward with rest0331      exact dBI with equal332  constructor333  . intro member334    have alternatives0 := insert.membership.forward with member335    rcases alternatives0 with equal0 | rest0336    . exact dCB with equal0337    . have alternatives1 := insert.membership.forward with rest0338      rcases alternatives1 with equal1 | rest1339      . exact dCA with equal1340      . have equal := singleton.membership.forward with rest1341        exact dCI with equal342  constructor343  . intro member344    have alternatives0 := insert.membership.forward with member345    rcases alternatives0 with equal0 | rest0346    . exact dFC with equal0347    . have alternatives1 := insert.membership.forward with rest0348      rcases alternatives1 with equal1 | rest1349      . exact dFB with equal1350      . have alternatives2 := insert.membership.forward with rest1351        rcases alternatives2 with equal2 | rest2352        . exact dFA with equal2353        . have equal := singleton.membership.forward with rest2354          exact dFI with equal355  . intro member356    have alternatives0 := insert.membership.forward with member357    rcases alternatives0 with equal0 | rest0358    . exact dGF with equal0359    . have alternatives1 := insert.membership.forward with rest0360      rcases alternatives1 with equal1 | rest1361      . exact dGC with equal1362      . have alternatives2 := insert.membership.forward with rest1363        rcases alternatives2 with equal2 | rest2364        . exact dGB with equal2365        . have alternatives3 := insert.membership.forward with rest2366          rcases alternatives3 with equal3 | rest3367          . exact dGA with equal3368          . have equal := singleton.membership.forward with rest3369            exact dGI with equal370371-- The six listed permutations are all of them: they are six distinct372-- permutations of 3, and 3 has 3! = 6 permutations.373theorem permutations.three374  shows permutations(3) = insert(cycleBackward, insert(cycleForward,375    insert(swapOneTwo, insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))376proof377  obtain ⟨freshA, freshB, freshC, freshF, freshG⟩ := permutations.three_fresh378  have finite := permutations.finite at 3 with (Finite.natural at 3)379  have subset : insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,380      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))) ⊆ permutations(3)381    intros p hp382    have alternatives0 := insert.membership.forward with hp383    rcases alternatives0 with equal0 | rest0384    . rw equal0385      exact cycleBackward.permutation386    . have alternatives1 := insert.membership.forward with rest0387      rcases alternatives1 with equal1 | rest1388      . rw equal1389        exact cycleForward.permutation390      . have alternatives2 := insert.membership.forward with rest1391        rcases alternatives2 with equal2 | rest2392        . rw equal2393          exact swapOneTwo.permutation394        . have alternatives3 := insert.membership.forward with rest2395          rcases alternatives3 with equal3 | rest3396          . rw equal3397            exact swapZeroTwo.permutation398          . have alternatives4 := insert.membership.forward with rest3399            rcases alternatives4 with equal4 | rest4400            . rw equal4401              exact swapZeroOne.permutation402            . have equal := singleton.membership.forward with rest4403              rw equal404              exact permutations.identity at 3405  have finite1 := Finite.singleton at identity(3)406  have finite2 := Finite.insert at {identity(3)}, swapZeroOne with finite1407  have finite3 := Finite.insert at insert(swapZeroOne, {identity(3)}), swapZeroTwo408    with finite2409  have finite4 := Finite.insert at insert(swapZeroTwo, insert(swapZeroOne,410    {identity(3)})), swapOneTwo with finite3411  have finite5 := Finite.insert at insert(swapOneTwo, insert(swapZeroTwo,412    insert(swapZeroOne, {identity(3)}))), cycleForward with finite4413  have count1 := cardinality.singleton at identity(3)414  have count2 := cardinality.insert at {identity(3)}, swapZeroOne with finite1, freshA415  have count3 := cardinality.insert at insert(swapZeroOne, {identity(3)}), swapZeroTwo416    with finite2, freshB417  have count4 := cardinality.insert at insert(swapZeroTwo, insert(swapZeroOne,418    {identity(3)})), swapOneTwo with finite3, freshC419  have count5 := cardinality.insert at insert(swapOneTwo, insert(swapZeroTwo,420    insert(swapZeroOne, {identity(3)}))), cycleForward with finite4, freshF421  have count6 := cardinality.insert at insert(cycleForward, insert(swapOneTwo,422    insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))), cycleBackward423    with finite5, freshG424  have same : cardinality(insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,425      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))) =426      cardinality(permutations(3))427    rw [count6, count5, count4, count3, count2, count1, permutations.three_count]428    compute429  have equal := cardinality.eq_subset with finite, subset, same430  symm at equal431  exact equal432433section Signs434variable (A add zero neg mul one : Set)435notation ring R := (A, add, zero, neg, mul, one)436hypothesis ring : IsCommRing(R)437438-- A transposition has sign -1: it is the exchange of the identity.439theorem permutationSign.transposition (n : Nat) (a b : Set)440  requires ha : a ∈ n441  requires hb : b ∈ n442  requires distinct : a ≠ b443  shows permutationSign(n, R, transposition(n, a, b)) = R[-R[1]]444proof445  have idPerm := permutations.identity at n446  have exchange := permutationSign.exchange at A, add, zero, neg, mul, one, n, a, b,447    identity(n) with ring, ha, hb, distinct, idPerm448  have value := permutationExchange.value at n, a, b, identity(n) with ha, hb, idPerm449  have swapFunction := transposition.function at n, a, b with ha, hb450  have left := compose.identity_left at transposition(n, a, b), n, n with swapFunction451  have signOne := permutationSign.identity at A, add, zero, neg, mul, one, n with ring452  rw [value, left, signOne] at exchange453  exact exchange454455end Signs456457-- The signs of the six permutations of 3: the identity has sign 1, the458-- transpositions -1, and the three-cycles, each one exchange away from a459-- transposition, -(-1).460theorem permutations.three_signs (A add zero neg mul one : Set)461  requires ring : IsCommRing(A, add, zero, neg, mul, one)462  shows permutationSign(3, A, add, zero, neg, mul, one, identity(3)) = one ∧463    permutationSign(3, A, add, zero, neg, mul, one, swapZeroOne) = neg(one) ∧464    permutationSign(3, A, add, zero, neg, mul, one, swapZeroTwo) = neg(one) ∧465    permutationSign(3, A, add, zero, neg, mul, one, swapOneTwo) = neg(one) ∧466    permutationSign(3, A, add, zero, neg, mul, one, cycleForward) = neg(neg(one)) ∧467    permutationSign(3, A, add, zero, neg, mul, one, cycleBackward) = neg(neg(one))468proof469  have signI := permutationSign.identity at A, add, zero, neg, mul, one, 3 with ring470  have signA := permutationSign.transposition at A, add, zero, neg, mul, one, 3, 0, 1471    with ring, three.zero_mem, three.one_mem, three.zero_ne_one472  have signB := permutationSign.transposition at A, add, zero, neg, mul, one, 3, 0, 2473    with ring, three.zero_mem, three.two_mem, three.zero_ne_two474  have signC := permutationSign.transposition at A, add, zero, neg, mul, one, 3, 1, 2475    with ring, three.one_mem, three.two_mem, three.one_ne_two476  have signSwap : permutationSign(3, A, add, zero, neg, mul, one, swapZeroOne) = neg(one)477    simp [swapZeroOne]478  have exchangeF := permutationSign.exchange at A, add, zero, neg, mul, one, 3, 1, 2,479    swapZeroOne with ring, three.one_mem, three.two_mem, three.one_ne_two,480    swapZeroOne.permutation481  have valueF := permutationExchange.value at 3, 1, 2, swapZeroOne482    with three.one_mem, three.two_mem, swapZeroOne.permutation483  have exchangeG := permutationSign.exchange at A, add, zero, neg, mul, one, 3, 0, 2,484    swapZeroOne with ring, three.zero_mem, three.two_mem, three.zero_ne_two,485    swapZeroOne.permutation486  have valueG := permutationExchange.value at 3, 0, 2, swapZeroOne487    with three.zero_mem, three.two_mem, swapZeroOne.permutation488  have signF : permutationSign(3, A, add, zero, neg, mul, one, cycleForward) =489      neg(neg(one))490    unfold cycleForward491    unfold swapOneTwo492    rw ← valueF493    rw [exchangeF, signSwap]494    rfl495  have signG : permutationSign(3, A, add, zero, neg, mul, one, cycleBackward) =496      neg(neg(one))497    unfold cycleBackward498    unfold swapZeroTwo499    rw ← valueG500    rw [exchangeG, signSwap]501    rfl502  unfold swapZeroOne503  unfold swapZeroTwo504  unfold swapOneTwo505  exact ⟨signI, signA, signB, signC, signF, signG⟩506507-- The product of the entries picked by a permutation of 3.508theorem permutationEntries.three_product (A add zero neg mul one M p : Set)509  requires ring : IsCommRing(A, add, zero, neg, mul, one)510  requires matrix : RingMatrix(3, A, M)511  requires permutation : p ∈ permutations(3)512  shows finiteRingProduct(3, A, add, zero, neg, mul, one, permutationEntries(3, A, M, p)) =513    call2(mul, call2(mul, call2(mul, one, M[0, p(0)]), M[1, p(1)]), M[2, p(2)])514proof515  have bijective := permutations.bijective with permutation516  have weights := permutationEntries.function at 3, A, M, p with matrix, bijective517  have enumeration := identity.bijective at 3518  have indexed := finiteRingProduct.enumeration at 3, A, add, zero, neg, mul, one,519    permutationEntries(3, A, M, p), identity(3), 3 with ring, weights, enumeration520  obtain ⟨i0, i1, i2⟩ := identity.three_values521  have e0 := permutationEntries.value at 3, A, M, p, 0 with matrix, bijective, three.zero_mem522  have e1 := permutationEntries.value at 3, A, M, p, 1 with matrix, bijective, three.one_mem523  have e2 := permutationEntries.value at 3, A, M, p, 2 with matrix, bijective, three.two_mem524  rw indexed525  simp [indexedRingProduct, i0, i1, i2, e0, e1, e2]526527-- The determinant of a 3 × 3 matrix is the sum of its six signed528-- permutation products, listed as the identity, the three transpositions,529-- and the two three-cycles.530theorem determinant.three (A add zero neg mul one M : Set)531  requires ring : IsCommRing(A, add, zero, neg, mul, one)532  requires matrix : RingMatrix(3, A, M)533  shows determinant(3, A, add, zero, neg, mul, one, M) =534    call2(add, call2(add, call2(add, call2(add, call2(add,535      call2(mul, one,536        call2(mul, call2(mul, call2(mul, one, M[0, 0]), M[1, 1]), M[2, 2])),537      call2(mul, neg(one),538        call2(mul, call2(mul, call2(mul, one, M[0, 1]), M[1, 0]), M[2, 2]))),539      call2(mul, neg(one),540        call2(mul, call2(mul, call2(mul, one, M[0, 2]), M[1, 1]), M[2, 0]))),541      call2(mul, neg(one),542        call2(mul, call2(mul, call2(mul, one, M[0, 0]), M[1, 2]), M[2, 1]))),543      call2(mul, neg(neg(one)),544        call2(mul, call2(mul, call2(mul, one, M[0, 1]), M[1, 2]), M[2, 0]))),545      call2(mul, neg(neg(one)),546        call2(mul, call2(mul, call2(mul, one, M[0, 2]), M[1, 0]), M[2, 1])))547proof548  have finite := Finite.natural at 3549  have terms := determinantTerms.function at 3, A, add, zero, neg, mul, one, M550    with ring, finite, matrix551  obtain ⟨freshA, freshB, freshC, freshF, freshG⟩ := permutations.three_fresh552  obtain ⟨signI, signA, signB, signC, signF, signG⟩ :=553    permutations.three_signs at A, add, zero, neg, mul, one with ring554  obtain ⟨i0, i1, i2⟩ := identity.three_values555  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values556  obtain ⟨b0, b1, b2⟩ := swapZeroTwo.values557  obtain ⟨c0, c1, c2⟩ := swapOneTwo.values558  obtain ⟨f0, f1, f2⟩ := cycleForward.values559  obtain ⟨g0, g1, g2⟩ := cycleBackward.values560  have idPerm := permutations.identity at 3561  have termI := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, identity(3)562    with ring, finite, matrix, idPerm563  have termA := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, swapZeroOne564    with ring, finite, matrix, swapZeroOne.permutation565  have termB := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, swapZeroTwo566    with ring, finite, matrix, swapZeroTwo.permutation567  have termC := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, swapOneTwo568    with ring, finite, matrix, swapOneTwo.permutation569  have termF := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, cycleForward570    with ring, finite, matrix, cycleForward.permutation571  have termG := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, cycleBackward572    with ring, finite, matrix, cycleBackward.permutation573  have productI := permutationEntries.three_product at A, add, zero, neg, mul, one, M,574    identity(3) with ring, matrix, idPerm575  have productA := permutationEntries.three_product at A, add, zero, neg, mul, one, M,576    swapZeroOne with ring, matrix, swapZeroOne.permutation577  have productB := permutationEntries.three_product at A, add, zero, neg, mul, one, M,578    swapZeroTwo with ring, matrix, swapZeroTwo.permutation579  have productC := permutationEntries.three_product at A, add, zero, neg, mul, one, M,580    swapOneTwo with ring, matrix, swapOneTwo.permutation581  have productF := permutationEntries.three_product at A, add, zero, neg, mul, one, M,582    cycleForward with ring, matrix, cycleForward.permutation583  have productG := permutationEntries.three_product at A, add, zero, neg, mul, one, M,584    cycleBackward with ring, matrix, cycleBackward.permutation585  rw [i0, i1, i2] at productI586  rw [a0, a1, a2] at productA587  rw [b0, b1, b2] at productB588  rw [c0, c1, c2] at productC589  rw [f0, f1, f2] at productF590  rw [g0, g1, g2] at productG591  have listed := permutations.three592  rw listed at terms593  have whole : insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,594      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))) ⊆595      insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,596      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))597    intros x hx598    exact hx599  have six := finiteRingSum.six at A, add, zero, neg, mul, one,600    determinantTerms(3, A, add, zero, neg, mul, one, M),601    insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,602      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))),603    identity(3), swapZeroOne, swapZeroTwo, swapOneTwo, cycleForward, cycleBackward604    with ring, terms, whole, freshA, freshB, freshC, freshF, freshG605  have listedFinite : Finite(insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,606      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))))607    rw ← listed608    exact permutations.finite at 3 with finite609  have restricted := restrict.domain_function at610    determinantTerms(3, A, add, zero, neg, mul, one, M),611    insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,612      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))), A,613    insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,614      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))) with terms, whole615  have values : ∀ x ∈ insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,616      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))),617      determinantTerms(3, A, add, zero, neg, mul, one, M)(x) =618      restrict(determinantTerms(3, A, add, zero, neg, mul, one, M),619        insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,620        insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))))(x)621    intros x hx622    have value := restrict.domain_apply at623      determinantTerms(3, A, add, zero, neg, mul, one, M),624      insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,625        insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))), A,626      insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,627        insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))), x with terms, whole, hx628    symm at value629    exact value630  have congruent := finiteRingSum.congr with ring, listedFinite, terms, restricted, values631  simp [determinant]632