Grace/Cumulus/Algebra/Ring/DeterminantZero.g17

Open in Workbench Download source

Imports

Determinant · FiniteLinearity

Declarations

• finiteRingProduct.zero_of_factor theorem derivation
• determinant.zero_row theorem derivation

Source

1-- A zero factor kills a finite product; a zero row kills a determinant (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Ring.DeterminantZero8import Determinant9import FiniteLinearity1011section Products12variable (V A add zero neg mul one w x : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)15hypothesis finite : Finite(V)16hypothesis weights : w : V → A17hypothesis member : x ∈ V18hypothesis vanishes : w(x) = R[0]1920theorem finiteRingProduct.zero_of_factor21  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = R[0]22proof23  have subset : V ∖ {x} ⊆ V by simp [Subset, difference.membership]24  have smaller := Finite.subset with finite, subset25  have restricted := restrict.domain_function at w, V, A, V ∖ {x} with *26  have rest := finiteRingProduct.closed at V ∖ {x}, A, add, zero, neg, mul, one, restrict(w, V ∖ {x}) with *27  have equation := finiteRingProduct.remove at V, A, add, zero, neg, mul, one, w, x with *28  rw [equation, vanishes]29  ring3031end Products3233section Determinants34variable (A add zero neg mul one M : Set)35notation ring R := (A, add, zero, neg, mul, one)36hypothesis ring : IsCommRing(R)3738theorem determinant.zero_row (n : Nat) (i : Set)39  requires matrix : RingMatrix(n, R, M)40  requires row : i ∈ n41  requires vanishes : ∀ j ∈ n, M[i, j] = R[0]42  shows determinant(n, R, M) = R[0]43proof44  have finite := Finite.natural with *45  have permutationsFinite := permutations.finite with finite46  have weights := determinantTerms.function at n, A, add, zero, neg, mul, one, M with *47  have zeroTerms : ∀ p ∈ permutations(n), determinantTerms(n, A, add, zero, neg, mul, one, M)(p) = R[0]48    intros p hp49    have permutation := permutations.mem_iff.forward with hp50    have injective := Bijective.injective with permutation51    have function := Injective.function with injective52    have column := FunctionBetween.apply_closed with function, row53    have entry := vanishes with p(i), column54    have entries := permutationEntries.function at n, A, M, p with *55    have value := permutationEntries.value at n, A, M, p, i with *56    have zeroEntry : permutationEntries(n, A, M, p)(i) = R[0] by rwa value57    have product := finiteRingProduct.zero_of_factor at n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p), i with *58    have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *59    have term := determinantTerms.value at n, A, add, zero, neg, mul, one, M, p with *60    rw [term, product]61    ring62  unfold determinant63  exact finiteRingSum.zero with ring, permutationsFinite, weights, zeroTerms6465end Determinants66