Grace/Cumulus/Algebra/Ring/DeterminantProduct.g17

Open in Workbench Download source

Imports

DeterminantRowPermutation · ProductExpansion · MatrixEntries

Declarations

Source

1-- The determinant is multiplicative: det(MN) = det(M) · det(N). Each2-- Leibniz term of MN is a product of row sums, which expands over the3-- functions f : n → n; interchanging the two sums leaves, for each f, the4-- determinant of the matrix whose rows are the rows f(i) of N, which5-- vanishes unless f is a permutation and is then sign(f) · det(N)6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Ring.DeterminantProduct12import DeterminantRowPermutation13import ProductExpansion14import MatrixEntries1516-- The pair weights of the entries of a product along a permutation p:17-- (i, k) ↦ M[i, k] · N[k, p(i)].18defgraph productPairWeights (n A add zero neg mul one M N p : Set) (q ∈ n × n) : A :=19  call2(mul, M[fst(q), snd(q)], N[snd(q), p(fst(q))])20requires ring : IsCommRing(A, add, zero, neg, mul, one)21requires matrixM : RingMatrix(n, A, M)22requires matrixN : RingMatrix(n, A, N)23requires function : p : n → n24proof25  obtain ⟨bound, i, hi, k, hk, shape⟩ := product.membership.forward with assumption26  have first : fst(q) = i27    rw shape28    exact fst.pair at i, k29  have second : snd(q) = k30    rw shape31    exact snd.pair at i, k32  rw [first, second]33  have image := FunctionBetween.apply_closed with function, hi34  have entryM := RingMatrix.entry at n, A, M, i, k with matrixM, hi, hk35  have entryN := RingMatrix.entry at n, A, N, k, p(i) with matrixN, hk, image36  have ordinary := IsCommRing.ring with ring37  exact IsRing.mul_closed with ordinary, entryM, entryN3839-- The matrix whose row i is the row f(i) of N.40defgraph selectedRows (n A N f : Set) (q ∈ n × n) : A := N[f(fst(q)), snd(q)]41requires matrixN : RingMatrix(n, A, N)42requires function : f : n → n43proof44  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with assumption45  have first : fst(q) = i46    rw shape47    exact fst.pair at i, j48  have second : snd(q) = j49    rw shape50    exact snd.pair at i, j51  rw [first, second]52  have image := FunctionBetween.apply_closed with function, hi53  exact RingMatrix.entry at n, A, N, f(i), j with matrixN, image, hj5455theorem selectedRows.matrix (n A N f : Set)56  requires matrixN : RingMatrix(n, A, N)57  requires function : f : n → n58  shows RingMatrix(n, A, selectedRows(n, A, N, f))59proof60  unfold RingMatrix61  exact selectedRows.function at n, A, N, f with matrixN, function6263theorem selectedRows.entry (n A N f i j : Set)64  requires matrixN : RingMatrix(n, A, N)65  requires function : f : n → n66  requires hi : i ∈ n67  requires hj : j ∈ n68  shows selectedRows(n, A, N, f)[i, j] = N[f(i), j]69proof70  have pair := product.pair at i, j, n, n with hi, hj71  have value := selectedRows.value at n, A, N, f, (i, j) with matrixN, function, pair72  rw [value, fst.pair, snd.pair]73  rfl7475-- The terms sign(p) · (∏ M[i, f(i)]) · (∏ N[f(i), p(i)]) indexed by a76-- permutation p and a function f.77defgraph doubleTerms (n A add zero neg mul one M N : Set)78    (q ∈ permutations(n) × functionSpace(n, n)) : A :=79  call2(mul, permutationSign(n, A, add, zero, neg, mul, one, fst(q)),80    call2(mul, functionProducts(n, n, A, add, zero, neg, mul, one, M)(snd(q)),81      functionProducts(n, n, A, add, zero, neg, mul, one, selectedRows(n, A, N, snd(q)))(fst(q))))82requires ring : IsCommRing(A, add, zero, neg, mul, one)83requires finite : Finite(n)84requires matrixM : RingMatrix(n, A, M)85requires matrixN : RingMatrix(n, A, N)86proof87  obtain ⟨bound, p, hp, f, hf, shape⟩ := product.membership.forward with assumption88  have first : fst(q) = p89    rw shape90    exact fst.pair at p, f91  have second : snd(q) = f92    rw shape93    exact snd.pair at p, f94  rw [first, second]95  have fFunction := functionSpace.mem_iff.forward with hf96  have pFunction := permutations.function with hp97  have pIn : p ∈ functionSpace(n, n) := functionSpace.mem_iff.backward with pFunction98  have matrixF := selectedRows.matrix at n, A, N, f with matrixN, fFunction99  unfold RingMatrix at matrixM100  unfold RingMatrix at matrixF101  have productsM := functionProducts.function at n, n, A, add, zero, neg, mul, one, M102    with ring, finite, matrixM103  have productsF := functionProducts.function at n, n, A, add, zero, neg, mul, one,104    selectedRows(n, A, N, f) with ring, finite, matrixF105  have aIn := FunctionBetween.apply_closed with productsM, hf106  have bIn := FunctionBetween.apply_closed with productsF, pIn107  have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, p with ring, finite108  have ordinary := IsCommRing.ring with ring109  have inner := IsRing.mul_closed with ordinary, aIn, bIn110  exact IsRing.mul_closed with ordinary, sign, inner111112section Product113variable (A add zero neg mul one : Set)114hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)115116-- A function n → n that is not a permutation repeats a value.117theorem functionSpace.collision (n : Nat) (f : Set)118  requires hf : f ∈ functionSpace(n, n)119  requires outside : ¬(f ∈ permutations(n))120  shows ∃ a ∈ n, ∃ b ∈ n, a ≠ b ∧ f(a) = f(b)121proof122  have function := functionSpace.mem_iff.forward with hf123  have finite := Finite.natural at n124  by_contra125  rename this => none126  have cancel : ∀ x ∈ n, ∀ y ∈ n, f(x) = f(y) → x = y127    intros x hx y hy same128    by_contra129    exact none with ⟨x, hx, y, hy, this, same⟩130  have injective := Injective.of_pointwise with function, cancel131  have bijective := Finite.self_injective_bijective with injective, finite132  have member := permutations.of_bijective with bijective133  exact outside with member134135-- The product of the entries of P along p, when P is the product of M and136-- N, is the sum over the functions f of the products of picked entries.137theorem productPairWeights.product (n : Nat) (M N P p : Set)138  requires matrixM : RingMatrix(n, A, M)139  requires matrixN : RingMatrix(n, A, N)140  requires matrixP : RingMatrix(n, A, P)141  requires entries : ∀ i ∈ n, ∀ j ∈ n,142    P[i, j] = matrixProductEntry(n, A, add, zero, neg, mul, one, M, N, i, j)143  requires hp : p ∈ permutations(n)144  shows finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, P, p)) =145    finiteRingSum(functionSpace(n, n), A, add, zero, neg, mul, one,146      functionProducts(n, n, A, add, zero, neg, mul, one,147        productPairWeights(n, A, add, zero, neg, mul, one, M, N, p)))148proof149  have finite := Finite.natural at n150  have pBijective := permutations.bijective with hp151  have pFunction := permutations.function with hp152  have weightsP := permutationEntries.function at n, A, P, p with matrixP, pBijective153  have pairs := productPairWeights.function at n, A, add, zero, neg, mul, one, M, N, p154    with ring, matrixM, matrixN, pFunction155  have rows := finiteRowSums.function at n, n, A, add, zero, neg, mul, one,156    productPairWeights(n, A, add, zero, neg, mul, one, M, N, p) with ring, finite, pairs157  have sameRows : ∀ i ∈ n, permutationEntries(n, A, P, p)(i) =158      finiteRowSums(n, n, A, add, zero, neg, mul, one,159        productPairWeights(n, A, add, zero, neg, mul, one, M, N, p))(i)160    intros i hi161    have image := FunctionBetween.apply_closed with pFunction, hi162    have entry := permutationEntries.value at n, A, P, p, i with matrixP, pBijective, hi163    have productEntry := entries with i, hi, p(i), image164    have rowValue := finiteRowSums.value at n, n, A, add, zero, neg, mul, one,165      productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), i with ring, finite, pairs, hi166    have rowWeights := finiteRowWeights.function at n, n, A,167      productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), i with pairs, hi168    have productWeights := matrixProductWeights.function at n, A, add, zero, neg, mul, one,169      M, N, i, p(i) with ring, matrixM, matrixN, hi, image170    have sameWeights : ∀ k ∈ n, matrixProductWeights(n, A, add, zero, neg, mul, one, M, N, i, p(i))(k) =171        finiteRowWeights(n, n, A, productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), i)(k)172      intros k hk173      have left := matrixProductWeights.value at n, A, add, zero, neg, mul, one, M, N, i, p(i), k174        with ring, matrixM, matrixN, hi, image, hk175      have right := finiteRowWeights.value at n, n, A,176        productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), i, k with pairs, hi, hk177      have pair := product.pair at i, k, n, n with hi, hk178      have pairValue := productPairWeights.value at n, A, add, zero, neg, mul, one, M, N, p, (i, k)179        with ring, matrixM, matrixN, pFunction, pair180      rw [left, right, pairValue, fst.pair, snd.pair]181      rfl182    have congruent := finiteRingSum.congr at n, A, add, zero, neg, mul, one,183      matrixProductWeights(n, A, add, zero, neg, mul, one, M, N, i, p(i)),184      finiteRowWeights(n, n, A, productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), i)185      with ring, finite, productWeights, rowWeights, sameWeights186    rw [entry, productEntry, rowValue]187    simp [matrixProductEntry]188  have congruent := finiteRingProduct.congr at n, A, add, zero, neg, mul, one,189    permutationEntries(n, A, P, p),190    finiteRowSums(n, n, A, add, zero, neg, mul, one,191      productPairWeights(n, A, add, zero, neg, mul, one, M, N, p))192    with ring, finite, weightsP, rows, sameRows193  have expansion := finiteRingProduct.row_sums at n, A, add, zero, neg, mul, one, n194    with ring, finite195  have expanded := expansion with productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), pairs196  rw [congruent, expanded]197  rfl198199-- The product of the picked pair weights splits into the product over M200-- and the product over the selected rows of N.201theorem productPairWeights.split (n : Nat) (M N p f : Set)202  requires matrixM : RingMatrix(n, A, M)203  requires matrixN : RingMatrix(n, A, N)204  requires hp : p ∈ permutations(n)205  requires hf : f ∈ functionSpace(n, n)206  shows functionProducts(n, n, A, add, zero, neg, mul, one,207      productPairWeights(n, A, add, zero, neg, mul, one, M, N, p))(f) =208    call2(mul, functionProducts(n, n, A, add, zero, neg, mul, one, M)(f),209      functionProducts(n, n, A, add, zero, neg, mul, one, selectedRows(n, A, N, f))(p))210proof211  have finite := Finite.natural at n212  have pFunction := permutations.function with hp213  have fFunction := functionSpace.mem_iff.forward with hf214  have pIn : p ∈ functionSpace(n, n) := functionSpace.mem_iff.backward with pFunction215  have pairs := productPairWeights.function at n, A, add, zero, neg, mul, one, M, N, p216    with ring, matrixM, matrixN, pFunction217  have matrixF := selectedRows.matrix at n, A, N, f with matrixN, fFunction218  have mFunction : M : n × n → A := matrixM219  have fMatrix : selectedRows(n, A, N, f) : n × n → A := matrixF220  have valuePairs := functionProducts.value at n, n, A, add, zero, neg, mul, one,221    productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), f with ring, finite, pairs, hf222  have valueM := functionProducts.value at n, n, A, add, zero, neg, mul, one, M, f223    with ring, finite, mFunction, hf224  have valueF := functionProducts.value at n, n, A, add, zero, neg, mul, one,225    selectedRows(n, A, N, f), p with ring, finite, fMatrix, pIn226  have pickedPairs := pickedWeights.function at n, n, A,227    productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), f with pairs, fFunction228  have pickedM := pickedWeights.function at n, n, A, M, f with mFunction, fFunction229  have pickedF := pickedWeights.function at n, n, A, selectedRows(n, A, N, f), p230    with fMatrix, pFunction231  have equations : ∀ i ∈ n,232      pickedWeights(n, n, A, productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), f)(i) =233      call2(mul, pickedWeights(n, n, A, M, f)(i),234        pickedWeights(n, n, A, selectedRows(n, A, N, f), p)(i))235    intros i hi236    have fi := FunctionBetween.apply_closed with fFunction, hi237    have pi := FunctionBetween.apply_closed with pFunction, hi238    have left := pickedWeights.value at n, n, A,239      productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), f, i with pairs, fFunction, hi240    have pair := product.pair at i, f(i), n, n with hi, fi241    have pairValue := productPairWeights.value at n, A, add, zero, neg, mul, one, M, N, p, (i, f(i))242      with ring, matrixM, matrixN, pFunction, pair243    have rightM := pickedWeights.value at n, n, A, M, f, i with mFunction, fFunction, hi244    have rightF := pickedWeights.value at n, n, A, selectedRows(n, A, N, f), p, i245      with fMatrix, pFunction, hi246    have selected := selectedRows.entry at n, A, N, f, i, p(i) with matrixN, fFunction, hi, pi247    rw [left, pairValue, fst.pair, snd.pair, rightM, rightF, selected]248    rfl249  have split := finiteRingProduct.mul at n, A, add, zero, neg, mul, one,250    pickedWeights(n, n, A, M, f), pickedWeights(n, n, A, selectedRows(n, A, N, f), p),251    pickedWeights(n, n, A, productPairWeights(n, A, add, zero, neg, mul, one, M, N, p), f)252    with ring, finite, pickedM, pickedF, pickedPairs, equations253  rw [valuePairs, valueM, valueF, split]254  rfl255256-- The inner sum over the permutations, for a fixed f, is the product over257-- M times the determinant of the selected rows of N.258theorem doubleTerms.column (n : Nat) (M N f : Set)259  requires matrixM : RingMatrix(n, A, M)260  requires matrixN : RingMatrix(n, A, N)261  requires hf : f ∈ functionSpace(n, n)262  shows finiteRingSum(permutations(n), A, add, zero, neg, mul, one,263      finiteRowWeights(functionSpace(n, n), permutations(n), A,264        transposedMatrix(permutations(n), functionSpace(n, n), A,265          doubleTerms(n, A, add, zero, neg, mul, one, M, N)), f)) =266    call2(mul, functionProducts(n, n, A, add, zero, neg, mul, one, M)(f),267      determinant(n, A, add, zero, neg, mul, one, selectedRows(n, A, N, f)))268proof269  have finite := Finite.natural at n270  have permutationsFinite := permutations.finite at n with finite271  have fFunction := functionSpace.mem_iff.forward with hf272  have matrixF := selectedRows.matrix at n, A, N, f with matrixN, fFunction273  have mFunction : M : n × n → A := matrixM274  have fMatrix : selectedRows(n, A, N, f) : n × n → A := matrixF275  have terms := doubleTerms.function at n, A, add, zero, neg, mul, one, M, N276    with ring, finite, matrixM, matrixN277  have transposed := transposedMatrix.function at permutations(n), functionSpace(n, n), A,278    doubleTerms(n, A, add, zero, neg, mul, one, M, N) with terms279  have rowWeights := finiteRowWeights.function at functionSpace(n, n), permutations(n), A,280    transposedMatrix(permutations(n), functionSpace(n, n), A,281      doubleTerms(n, A, add, zero, neg, mul, one, M, N)), f with transposed, hf282  have termsF := determinantTerms.function at n, A, add, zero, neg, mul, one,283    selectedRows(n, A, N, f) with ring, finite, matrixF284  have productsM := functionProducts.function at n, n, A, add, zero, neg, mul, one, M285    with ring, finite, mFunction286  have aIn := FunctionBetween.apply_closed with productsM, hf287  have values : ∀ p ∈ permutations(n),288      finiteRowWeights(functionSpace(n, n), permutations(n), A,289        transposedMatrix(permutations(n), functionSpace(n, n), A,290          doubleTerms(n, A, add, zero, neg, mul, one, M, N)), f)(p) =291      call2(mul, functionProducts(n, n, A, add, zero, neg, mul, one, M)(f),292        determinantTerms(n, A, add, zero, neg, mul, one, selectedRows(n, A, N, f))(p))293    intros p hp294    have pFunction := permutations.function with hp295    have pBijective := permutations.bijective with hp296    have pIn : p ∈ functionSpace(n, n) := functionSpace.mem_iff.backward with pFunction297    have rowValue := finiteRowWeights.value at functionSpace(n, n), permutations(n), A,298      transposedMatrix(permutations(n), functionSpace(n, n), A,299        doubleTerms(n, A, add, zero, neg, mul, one, M, N)), f, p with transposed, hf, hp300    have swap := transposedMatrix.pair at permutations(n), functionSpace(n, n), A,301      doubleTerms(n, A, add, zero, neg, mul, one, M, N), p, f with terms, hp, hf302    have pair := product.pair at p, f, permutations(n), functionSpace(n, n) with hp, hf303    have termValue := doubleTerms.value at n, A, add, zero, neg, mul, one, M, N, (p, f)304      with ring, finite, matrixM, matrixN, pair305    have detTerm := determinantTerms.value at n, A, add, zero, neg, mul, one,306      selectedRows(n, A, N, f), p with ring, finite, matrixF, hp307    have valueF := functionProducts.value at n, n, A, add, zero, neg, mul, one,308      selectedRows(n, A, N, f), p with ring, finite, fMatrix, pIn309    have pickedF := pickedWeights.function at n, n, A, selectedRows(n, A, N, f), p310      with fMatrix, pFunction311    have entriesF := permutationEntries.function at n, A, selectedRows(n, A, N, f), p312      with matrixF, pBijective313    have sameEntries : ∀ i ∈ n, permutationEntries(n, A, selectedRows(n, A, N, f), p)(i) =314        pickedWeights(n, n, A, selectedRows(n, A, N, f), p)(i)315      intros i hi316      have left := permutationEntries.value at n, A, selectedRows(n, A, N, f), p, i317        with matrixF, pBijective, hi318      have right := pickedWeights.value at n, n, A, selectedRows(n, A, N, f), p, i319        with fMatrix, pFunction, hi320      rw [left, right]321      rfl322    have congruent := finiteRingProduct.congr at n, A, add, zero, neg, mul, one,323      permutationEntries(n, A, selectedRows(n, A, N, f), p),324      pickedWeights(n, n, A, selectedRows(n, A, N, f), p)325      with ring, finite, entriesF, pickedF, sameEntries326    have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, p with ring, finite327    have bIn := finiteRingProduct.closed at n, A, add, zero, neg, mul, one,328      pickedWeights(n, n, A, selectedRows(n, A, N, f), p) with ring, finite, pickedF329    rw [rowValue, swap, termValue, fst.pair, snd.pair, detTerm, congruent, valueF]330    ring331  have scaled := finiteRingSum.scale_eq at permutations(n), A, add, zero, neg, mul, one,332    determinantTerms(n, A, add, zero, neg, mul, one, selectedRows(n, A, N, f)),333    finiteRowWeights(functionSpace(n, n), permutations(n), A,334      transposedMatrix(permutations(n), functionSpace(n, n), A,335        doubleTerms(n, A, add, zero, neg, mul, one, M, N)), f),336    functionProducts(n, n, A, add, zero, neg, mul, one, M)(f)337    with ring, permutationsFinite, termsF, rowWeights, aIn, values338  rw scaled339  unfold determinant340  rfl341342-- The determinant of a product matrix is the product of the determinants.343theorem determinant.product (n : Nat) (M N P : Set)344  requires matrixM : RingMatrix(n, A, M)345  requires matrixN : RingMatrix(n, A, N)346  requires matrixP : RingMatrix(n, A, P)347  requires entries : ∀ i ∈ n, ∀ j ∈ n,348    P[i, j] = matrixProductEntry(n, A, add, zero, neg, mul, one, M, N, i, j)349  shows determinant(n, A, add, zero, neg, mul, one, P) =350    call2(mul, determinant(n, A, add, zero, neg, mul, one, M),351      determinant(n, A, add, zero, neg, mul, one, N))352proof353  have finite := Finite.natural at n354  have permutationsFinite := permutations.finite at n with finite355  have spaceFinite := functionSpace.finite at n, n with finite, finite356  have mFunction : M : n × n → A := matrixM357  have ordinary := IsCommRing.ring with ring358  have termsP := determinantTerms.function at n, A, add, zero, neg, mul, one, P359    with ring, finite, matrixP360  have termsM := determinantTerms.function at n, A, add, zero, neg, mul, one, M361    with ring, finite, matrixM362  have terms := doubleTerms.function at n, A, add, zero, neg, mul, one, M, N363    with ring, finite, matrixM, matrixN364  have rows := finiteRowSums.function at permutations(n), functionSpace(n, n), A, add, zero,365    neg, mul, one, doubleTerms(n, A, add, zero, neg, mul, one, M, N) with ring, spaceFinite, terms366  have productsM := functionProducts.function at n, n, A, add, zero, neg, mul, one, M367    with ring, finite, mFunction368  have detN := determinant.closed at A, add, zero, neg, mul, one, N, n with ring, matrixN369  -- Each term of P is the row sum of the double terms at p.370  have rowValues : ∀ p ∈ permutations(n),371      determinantTerms(n, A, add, zero, neg, mul, one, P)(p) =372      finiteRowSums(permutations(n), functionSpace(n, n), A, add, zero, neg, mul, one,373        doubleTerms(n, A, add, zero, neg, mul, one, M, N))(p)374    intros p hp375    have pFunction := permutations.function with hp376    have termP := determinantTerms.value at n, A, add, zero, neg, mul, one, P, p377      with ring, finite, matrixP, hp378    have expansion := productPairWeights.product at A, add, zero, neg, mul, one, n, M, N, P, p379      with ring, matrixM, matrixN, matrixP, entries, hp380    have rowValue := finiteRowSums.value at permutations(n), functionSpace(n, n), A, add, zero,381      neg, mul, one, doubleTerms(n, A, add, zero, neg, mul, one, M, N), p382      with ring, spaceFinite, terms, hp383    have rowWeights := finiteRowWeights.function at permutations(n), functionSpace(n, n), A,384      doubleTerms(n, A, add, zero, neg, mul, one, M, N), p with terms, hp385    have pairs := productPairWeights.function at n, A, add, zero, neg, mul, one, M, N, p386      with ring, matrixM, matrixN, pFunction387    have products := functionProducts.function at n, n, A, add, zero, neg, mul, one,388      productPairWeights(n, A, add, zero, neg, mul, one, M, N, p) with ring, finite, pairs389    have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, p with ring, finite390    have scaledValues : ∀ f ∈ functionSpace(n, n),391        finiteRowWeights(permutations(n), functionSpace(n, n), A,392          doubleTerms(n, A, add, zero, neg, mul, one, M, N), p)(f) =393        call2(mul, permutationSign(n, A, add, zero, neg, mul, one, p),394          functionProducts(n, n, A, add, zero, neg, mul, one,395            productPairWeights(n, A, add, zero, neg, mul, one, M, N, p))(f))396      intros f hf397      have left := finiteRowWeights.value at permutations(n), functionSpace(n, n), A,398        doubleTerms(n, A, add, zero, neg, mul, one, M, N), p, f with terms, hp, hf399      have pair := product.pair at p, f, permutations(n), functionSpace(n, n) with hp, hf400      have termValue := doubleTerms.value at n, A, add, zero, neg, mul, one, M, N, (p, f)401        with ring, finite, matrixM, matrixN, pair402      have split := productPairWeights.split at A, add, zero, neg, mul, one, n, M, N, p, f403        with ring, matrixM, matrixN, hp, hf404      rw [left, termValue, fst.pair, snd.pair, split]405      rfl406    have scaled := finiteRingSum.scale_eq at functionSpace(n, n), A, add, zero, neg, mul, one,407      functionProducts(n, n, A, add, zero, neg, mul, one,408        productPairWeights(n, A, add, zero, neg, mul, one, M, N, p)),409      finiteRowWeights(permutations(n), functionSpace(n, n), A,410        doubleTerms(n, A, add, zero, neg, mul, one, M, N), p),411      permutationSign(n, A, add, zero, neg, mul, one, p)412      with ring, spaceFinite, products, rowWeights, sign, scaledValues413    rw [termP, expansion, rowValue, scaled]414    rfl415  have congruent := finiteRingSum.congr at permutations(n), A, add, zero, neg, mul, one,416    determinantTerms(n, A, add, zero, neg, mul, one, P),417    finiteRowSums(permutations(n), functionSpace(n, n), A, add, zero, neg, mul, one,418      doubleTerms(n, A, add, zero, neg, mul, one, M, N))419    with ring, permutationsFinite, termsP, rows, rowValues420  have interchange := finiteDoubleSum.interchange at permutations(n), functionSpace(n, n), A,421    add, zero, neg, mul, one, doubleTerms(n, A, add, zero, neg, mul, one, M, N)422    with ring, permutationsFinite, spaceFinite, terms423  have transposed := transposedMatrix.function at permutations(n), functionSpace(n, n), A,424    doubleTerms(n, A, add, zero, neg, mul, one, M, N) with terms425  have rowsT := finiteRowSums.function at functionSpace(n, n), permutations(n), A, add, zero,426    neg, mul, one, transposedMatrix(permutations(n), functionSpace(n, n), A,427      doubleTerms(n, A, add, zero, neg, mul, one, M, N)) with ring, permutationsFinite, transposed428  have permutationsSubset : permutations(n) ⊆ functionSpace(n, n)429    intros p hp430    exact functionSpace.mem_iff.backward with (permutations.function with hp)431  have restrictedRows := restrict.domain_function at432    finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,433      transposedMatrix(permutations(n), functionSpace(n, n), A,434        doubleTerms(n, A, add, zero, neg, mul, one, M, N))), functionSpace(n, n), A,435    permutations(n) with rowsT, permutationsSubset436  -- The column at f is the product over M times the determinant of the437  -- selected rows of N.438  have columns : ∀ f ∈ functionSpace(n, n),439      finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,440        transposedMatrix(permutations(n), functionSpace(n, n), A,441          doubleTerms(n, A, add, zero, neg, mul, one, M, N)))(f) =442      call2(mul, functionProducts(n, n, A, add, zero, neg, mul, one, M)(f),443        determinant(n, A, add, zero, neg, mul, one, selectedRows(n, A, N, f)))444    intros f hf445    have rowValue := finiteRowSums.value at functionSpace(n, n), permutations(n), A, add, zero,446      neg, mul, one, transposedMatrix(permutations(n), functionSpace(n, n), A,447        doubleTerms(n, A, add, zero, neg, mul, one, M, N)), f448      with ring, permutationsFinite, transposed, hf449    have column := doubleTerms.column at A, add, zero, neg, mul, one, n, M, N, f450      with ring, matrixM, matrixN, hf451    rw [rowValue, column]452    rfl453  have agreement : ∀ f ∈ permutations(n),454      finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,455        transposedMatrix(permutations(n), functionSpace(n, n), A,456          doubleTerms(n, A, add, zero, neg, mul, one, M, N)))(f) =457      restrict(finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,458        transposedMatrix(permutations(n), functionSpace(n, n), A,459          doubleTerms(n, A, add, zero, neg, mul, one, M, N))), permutations(n))(f)460    intros f hf461    have value := restrict.domain_apply at462      finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,463        transposedMatrix(permutations(n), functionSpace(n, n), A,464          doubleTerms(n, A, add, zero, neg, mul, one, M, N))), functionSpace(n, n), A,465      permutations(n), f with rowsT, permutationsSubset, hf466    symm at value467    exact value468  -- Outside the permutations a column vanishes: two rows of the selected469  -- matrix coincide.470  have vanishing : ∀ f ∈ functionSpace(n, n), ¬(f ∈ permutations(n)) →471      finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,472        transposedMatrix(permutations(n), functionSpace(n, n), A,473          doubleTerms(n, A, add, zero, neg, mul, one, M, N)))(f) = zero474    intros f hf outside475    have column := columns with f, hf476    have fFunction := functionSpace.mem_iff.forward with hf477    have matrixF := selectedRows.matrix at n, A, N, f with matrixN, fFunction478    obtain ⟨a, ha, b, hb, distinct, same⟩ := functionSpace.collision at A, add, zero, neg, mul,479      one, n, f with ring, hf, outside480    have equalRows : ∀ j ∈ n, selectedRows(n, A, N, f)[a, j] = selectedRows(n, A, N, f)[b, j]481      intros j hj482      have left := selectedRows.entry at n, A, N, f, a, j with matrixN, fFunction, ha, hj483      have right := selectedRows.entry at n, A, N, f, b, j with matrixN, fFunction, hb, hj484      rw [left, right, same]485      rfl486    have vanish := determinant.equal_rows at A, add, zero, neg, mul, one, n, a, b,487      selectedRows(n, A, N, f) with ring, matrixF, ha, hb, distinct, equalRows488    have aIn := FunctionBetween.apply_closed with productsM, hf489    have annihilate := IsRing.mul_zero at A, add, zero, neg, mul, one,490      functionProducts(n, n, A, add, zero, neg, mul, one, M)(f) with ordinary, aIn491    rw [column, vanish, annihilate]492    rfl493  have extension := finiteRingSum.zero_extension at functionSpace(n, n), permutations(n), A,494    add, zero, neg, mul, one,495    finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,496      transposedMatrix(permutations(n), functionSpace(n, n), A,497        doubleTerms(n, A, add, zero, neg, mul, one, M, N))),498    restrict(finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,499      transposedMatrix(permutations(n), functionSpace(n, n), A,500        doubleTerms(n, A, add, zero, neg, mul, one, M, N))), permutations(n))501    with ring, spaceFinite, rowsT, restrictedRows, permutationsSubset, agreement, vanishing502  -- On the permutations the column at f is det(N) times the term of M at f.503  have commutative := IsCommRing.commutative with ring504  unfold Commutative at commutative505  have scaledTerms : ∀ f ∈ permutations(n),506      restrict(finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,507        transposedMatrix(permutations(n), functionSpace(n, n), A,508          doubleTerms(n, A, add, zero, neg, mul, one, M, N))), permutations(n))(f) =509      call2(mul, determinant(n, A, add, zero, neg, mul, one, N),510        determinantTerms(n, A, add, zero, neg, mul, one, M)(f))511    intros f hf512    have fIn := permutationsSubset with f, hf513    have fFunction := permutations.function with hf514    have fBijective := permutations.bijective with hf515    have agree := agreement with f, hf516    have column := columns with f, fIn517    have matrixF := selectedRows.matrix at n, A, N, f with matrixN, fFunction518    have selected : ∀ i ∈ n, ∀ j ∈ n, selectedRows(n, A, N, f)[i, j] = N[f(i), j]519      intros i hi j hj520      exact selectedRows.entry at n, A, N, f, i, j with matrixN, fFunction, hi, hj521    have permuted := determinant.row_permutation at A, add, zero, neg, mul, one, n, N,522      selectedRows(n, A, N, f), f with ring, matrixN, matrixF, hf, selected523    have termM := determinantTerms.value at n, A, add, zero, neg, mul, one, M, f524      with ring, finite, matrixM, hf525    have valueM := functionProducts.value at n, n, A, add, zero, neg, mul, one, M, f526      with ring, finite, mFunction, fIn527    have entriesM := permutationEntries.function at n, A, M, f with matrixM, fBijective528    have pickedM := pickedWeights.function at n, n, A, M, f with mFunction, fFunction529    have sameEntries : ∀ i ∈ n, pickedWeights(n, n, A, M, f)(i) = permutationEntries(n, A, M, f)(i)530      intros i hi531      have left := pickedWeights.value at n, n, A, M, f, i with mFunction, fFunction, hi532      have right := permutationEntries.value at n, A, M, f, i with matrixM, fBijective, hi533      rw [left, right]534      rfl535    have congruentM := finiteRingProduct.congr at n, A, add, zero, neg, mul, one,536      pickedWeights(n, n, A, M, f), permutationEntries(n, A, M, f)537      with ring, finite, pickedM, entriesM, sameEntries538    have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, f with ring, finite539    have productIn := finiteRingProduct.closed at n, A, add, zero, neg, mul, one,540      permutationEntries(n, A, M, f) with ring, finite, entriesM541    rw [← agree, column, permuted, valueM, congruentM, termM]542    ring543  have scaled := finiteRingSum.scale_eq at permutations(n), A, add, zero, neg, mul, one,544    determinantTerms(n, A, add, zero, neg, mul, one, M),545    restrict(finiteRowSums(functionSpace(n, n), permutations(n), A, add, zero, neg, mul, one,546      transposedMatrix(permutations(n), functionSpace(n, n), A,547        doubleTerms(n, A, add, zero, neg, mul, one, M, N))), permutations(n)),548    determinant(n, A, add, zero, neg, mul, one, N)549    with ring, permutationsFinite, termsM, restrictedRows, detN, scaledTerms550  have detM := determinant.closed at A, add, zero, neg, mul, one, M, n with ring, matrixM551  have swap := commutative with determinant(n, A, add, zero, neg, mul, one, N), detN,552    determinant(n, A, add, zero, neg, mul, one, M), detM553  have detP : determinant(n, A, add, zero, neg, mul, one, P) =554      finiteRingSum(permutations(n), A, add, zero, neg, mul, one,555        determinantTerms(n, A, add, zero, neg, mul, one, P))556    unfold determinant557    rfl558  have detMvalue : determinant(n, A, add, zero, neg, mul, one, M) =559      finiteRingSum(permutations(n), A, add, zero, neg, mul, one,560        determinantTerms(n, A, add, zero, neg, mul, one, M))561    unfold determinant562    rfl563  unfold finiteDoubleSum at interchange564  rw [detP, congruent, interchange, extension, scaled, ← detMvalue, swap]565  rfl566567end Product568569section Bundled570variable (R : Set) (n : Nat)571hypothesis comm : CommRing(R)572573-- The determinant is multiplicative on the matrix ring.574theorem Matrix.det_mul (M N P : R ^ n × n)575  requires product : P = M * N576  shows det(P) = det(M) * det(N)577proof578  have parts := CommRing.parts with comm579  have matrixM : RingMatrix(n, Ring.carrier(R), M)580    unfold RingMatrix581    exact Matrix.function with *582  have matrixN : RingMatrix(n, Ring.carrier(R), N)583    unfold RingMatrix584    exact Matrix.function with *585  have matrixP : RingMatrix(n, Ring.carrier(R), P)586    unfold RingMatrix587    exact Matrix.function with *588  have entries : ∀ i ∈ n, ∀ j ∈ n, P[i, j] = matrixProductEntry(n, Ring.carrier(R),589      Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M, N, i, j)590    intros i hi j hj591    have entry := matrixRing.mul_entry at R, n, M, N, i, j with comm, hi, hj592    rw product593    exact entry594  exact determinant.product at Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R),595    Ring.mul(R), Ring.one(R), n, M, N, P with parts, matrixM, matrixN, matrixP, entries596597end Bundled598