-- A zero factor kills a finite product; a zero row kills a determinant (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.DeterminantZero
import Determinant
import FiniteLinearity

section Products
variable (V A add zero neg mul one w x : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)
hypothesis finite : Finite(V)
hypothesis weights : w : V → A
hypothesis member : x ∈ V
hypothesis vanishes : w(x) = R[0]

theorem finiteRingProduct.zero_of_factor
  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = R[0]
proof
  have subset : V ∖ {x} ⊆ V by simp [Subset, difference.membership]
  have smaller := Finite.subset with finite, subset
  have restricted := restrict.domain_function at w, V, A, V ∖ {x} with *
  have rest := finiteRingProduct.closed at V ∖ {x}, A, add, zero, neg, mul, one, restrict(w, V ∖ {x}) with *
  have equation := finiteRingProduct.remove at V, A, add, zero, neg, mul, one, w, x with *
  rw [equation, vanishes]
  ring

end Products

section Determinants
variable (A add zero neg mul one M : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)

theorem determinant.zero_row (n : Nat) (i : Set)
  requires matrix : RingMatrix(n, R, M)
  requires row : i ∈ n
  requires vanishes : ∀ j ∈ n, M[i, j] = R[0]
  shows determinant(n, R, M) = R[0]
proof
  have finite := Finite.natural with *
  have permutationsFinite := permutations.finite with finite
  have weights := determinantTerms.function at n, A, add, zero, neg, mul, one, M with *
  have zeroTerms : ∀ p ∈ permutations(n), determinantTerms(n, A, add, zero, neg, mul, one, M)(p) = R[0]
    intros p hp
    have permutation := permutations.mem_iff.forward with hp
    have injective := Bijective.injective with permutation
    have function := Injective.function with injective
    have column := FunctionBetween.apply_closed with function, row
    have entry := vanishes with p(i), column
    have entries := permutationEntries.function at n, A, M, p with *
    have value := permutationEntries.value at n, A, M, p, i with *
    have zeroEntry : permutationEntries(n, A, M, p)(i) = R[0] by rwa value
    have product := finiteRingProduct.zero_of_factor at n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p), i with *
    have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *
    have term := determinantTerms.value at n, A, add, zero, neg, mul, one, M, p with *
    rw [term, product]
    ring
  unfold determinant
  exact finiteRingSum.zero with ring, permutationsFinite, weights, zeroTerms

end Determinants