Imports
/-
Copyright (c) 2026 Robert Sneiderman. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Sneiderman
-/
module
public import Physlib.Mathematics.KroneckerDelta.Basic
public import Mathlib.LinearAlgebra.Matrix.SchurComplementContraction identities for the generalized Kronecker delta
i. Overview
This file proves the combinatorial contraction facts for the generalizedKroneckerDelta
(defined in Physlib.Mathematics.KroneckerDelta.Basic). Everything here is purely about the
abstract generalized Kronecker delta on a finite type; no tensor or physics content appears.
These facts are the reusable backbone of the Levi-Civita epsilon-epsilon contraction
identities proved in Physlib.Relativity.Tensors.LeviCivita.Contractions.
The central fact is that summing a generalizedKroneckerDelta over one shared index lowers
its rank by one and multiplies it by card α - n (generalizedKroneckerDelta_sum_snoc).
Iterating that fact, together with the product identity
generalizedKroneckerDelta μ ν = generalizedKroneckerDelta μ id * generalizedKroneckerDelta ν id
(generalizedKroneckerDelta_mul), gives the fully-, singly-, and doubly-free
contractions sum_generalizedKroneckerDelta_self, sum_generalizedKroneckerDelta_cons, and
sum_generalizedKroneckerDelta_cons₂ over Fin 4.
The proof of generalizedKroneckerDelta_sum_snoc borders the delta matrix with the appended
index (a Schur-complement reduction) and then applies the ring-general rank-one determinant
update lemma Matrix.det_add_rankOne, which is proved here because Mathlib only provides the
matrix determinant lemma when det A is a unit and Kronecker-delta matrices are singular.
ii. Key results
generalizedKroneckerDelta_sum_snoc : summing over one shared index lowers the rank by one.
sum_generalizedKroneckerDelta_mul_self, sum_generalizedKroneckerDelta_mul_cons,
sum_generalizedKroneckerDelta_mul_cons₂ : the fully-, singly-, and doubly-free symbol-level
contractions over Fin 4.
iii. Table of contents
A. The rank-one determinant update
B. Contraction identities
iv. References
@[expose] public sectionA. The rank-one determinant update
Expanding the determinant of a rank-one row update over a finite set of rows.
For i ∈ s the row A i is replaced by A i + w i • b; the other rows are untouched.
insert ι:Type u_1inst✝²:DecidableEq ιinst✝¹:Fintype ιR:Type u_2inst✝:CommRing RA:Matrix ι ι Rw:ι → Rb:ι → Ri₀:ιs:Finset ιhi₀:i₀ ∉ sMs:Matrix ι ι R := A + of fun i j => (if i ∈ s then w i else 0) * b jih:Ms.det = A.det + ∑ i ∈ s, w i * (A.updateRow i b).dethMs:Ms = A + of fun i j => (if i ∈ s then w i else 0) * b jhrow:Ms i₀ = A i₀key:(A + of fun i j => (if i ∈ insert i₀ s then w i else 0) * b j) = Ms.updateRow i₀ (A i₀ + w i₀ • b)h1:(Ms.updateRow i₀ (A i₀)).det = Ms.deth2:(Ms.updateRow i₀ b).det = (A.updateRow i₀ b).det⊢ A.det + ∑ i ∈ s, w i * (A.updateRow i b).det + w i₀ * (A.updateRow i₀ b).det =
A.det + (w i₀ * (A.updateRow i₀ b).det + ∑ x ∈ s, w x * (A.updateRow x b).det)
ring All goals completed! 🐙
Rank-one determinant update (the ring-general matrix determinant lemma for an outer
product, valid even when A is singular). Adding the rank-one matrix w ⊗ b to A changes the
determinant by ∑ i, w i * det (A.updateRow i b).
Mathlib only provides this when det A is a unit (Matrix.det_add_replicateCol_mul_replicateRow);
the singular case is needed here because Kronecker-delta matrices are typically singular.
private lemma det_add_rankOne {ι : Type*} [DecidableEq ι] [Fintype ι] {R : Type*}
[CommRing R] (A : Matrix ι ι R) (w b : ι → R) :
(A + Matrix.of fun i j => w i * b j).det = A.det + ∑ i, w i * (A.updateRow i b).det := by ι:Type u_1inst✝²:DecidableEq ιinst✝¹:Fintype ιR:Type u_2inst✝:CommRing RA:Matrix ι ι Rw:ι → Rb:ι → R⊢ (A + of fun i j => w i * b j).det = A.det + ∑ i, w i * (A.updateRow i b).det
have h := det_add_rankOne_aux A w b Finset.univ ι:Type u_1inst✝²:DecidableEq ιinst✝¹:Fintype ιR:Type u_2inst✝:CommRing RA:Matrix ι ι Rw:ι → Rb:ι → Rh:(A + of fun i j => (if i ∈ Finset.univ then w i else 0) * b j).det = A.det + ∑ i, w i * (A.updateRow i b).det⊢ (A + of fun i j => w i * b j).det = A.det + ∑ i, w i * (A.updateRow i b).det
simpa using h All goals completed! 🐙B. Contraction identities
The product of two Levi-Civita-type symbols is a generalized Kronecker delta:
δ^{μ}_{·} · δ^{ν}_{·} = δ^{μ}_{ν}, where each single factor is a Kronecker matrix against the
identity. This is the Lean form of ε^{μ₁…μₙ} ε_{ν₁…νₙ} = δ^{μ₁…μₙ}_{ν₁…νₙ}.
lemma generalizedKroneckerDelta_mul (μ ν : α → α) :
generalizedKroneckerDelta μ id * generalizedKroneckerDelta ν id
= generalizedKroneckerDelta μ ν := by α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ generalizedKroneckerDelta μ id * generalizedKroneckerDelta ν id = generalizedKroneckerDelta μ ν
rw [show generalizedKroneckerDelta ν id
= (Matrix.of fun i j => ((kroneckerDelta (ν i) (id j) : ℕ) : ℤ)).det from rfl, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ generalizedKroneckerDelta μ id * (of fun i j => ↑δ[ν i,id j]).det = generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = (of fun i j => ↑δ[μ i,ν j]).det
← Matrix.det_transpose, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ generalizedKroneckerDelta μ id * (of fun i j => ↑δ[ν i,id j])ᵀ.det = generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = (of fun i j => ↑δ[μ i,ν j]).det
show generalizedKroneckerDelta μ id
= (Matrix.of fun i j => ((kroneckerDelta (μ i) (id j) : ℕ) : ℤ)).det from rfl, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ (of fun i j => ↑δ[μ i,id j]).det * (of fun i j => ↑δ[ν i,id j])ᵀ.det = generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = (of fun i j => ↑δ[μ i,ν j]).det
← Matrix.det_mul, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = (of fun i j => ↑δ[μ i,ν j]).det
show generalizedKroneckerDelta μ ν
= (Matrix.of fun i j => ((kroneckerDelta (μ i) (ν j) : ℕ) : ℤ)).det from rfl α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = (of fun i j => ↑δ[μ i,ν j]).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = (of fun i j => ↑δ[μ i,ν j]).det] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ).det = (of fun i j => ↑δ[μ i,ν j]).det
congr 1 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → α⊢ (of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ = of fun i j => ↑δ[μ i,ν j]
ext i j α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ((of fun i j => ↑δ[μ i,id j]) * (of fun i j => ↑δ[ν i,id j])ᵀ) i j = of (fun i j => ↑δ[μ i,ν j]) i j
rw [Matrix.mul_apply α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ j_1, of (fun i j => ↑δ[μ i,id j]) i j_1 * (of fun i j => ↑δ[ν i,id j])ᵀ j_1 j = of (fun i j => ↑δ[μ i,ν j]) i j α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ j_1, of (fun i j => ↑δ[μ i,id j]) i j_1 * (of fun i j => ↑δ[ν i,id j])ᵀ j_1 j = of (fun i j => ↑δ[μ i,ν j]) i j] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ j_1, of (fun i j => ↑δ[μ i,id j]) i j_1 * (of fun i j => ↑δ[ν i,id j])ᵀ j_1 j = of (fun i j => ↑δ[μ i,ν j]) i j
simp only [Matrix.of_apply, Matrix.transpose_apply, id_eq, ← Nat.cast_mul] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ x, ↑(δ[μ i,x] * δ[ν j,x]) = ↑δ[μ i,ν j]
rw [← Nat.cast_sum α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ↑(∑ x, δ[μ i,x] * δ[ν j,x]) = ↑δ[μ i,ν j] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ↑(∑ x, δ[μ i,x] * δ[ν j,x]) = ↑δ[μ i,ν j]] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ↑(∑ x, δ[μ i,x] * δ[ν j,x]) = ↑δ[μ i,ν j]
congr 1 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ x, δ[μ i,x] * δ[ν j,x] = δ[μ i,ν j]
rw [Finset.sum_congr rfl fun k _ => by α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:αk:αx✝:k ∈ Finset.univ⊢ δ[μ i,k] * δ[ν j,k] = ?m.169 k α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ k, δ[μ i,k] * δ[k,ν j] = δ[μ i,ν j] rw [KroneckerDelta.symm (ν j) k α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:αk:αx✝:k ∈ Finset.univ⊢ δ[μ i,k] * δ[k,ν j] = ?m.169 k All goals completed! 🐙 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ k, δ[μ i,k] * δ[k,ν j] = δ[μ i,ν j]] All goals completed! 🐙 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ k, δ[μ i,k] * δ[k,ν j] = δ[μ i,ν j]] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α → αν:α → αi:αj:α⊢ ∑ k, δ[μ i,k] * δ[k,ν j] = δ[μ i,ν j]
exact KroneckerDelta.sum_mul (μ i) (ν j) All goals completed! 🐙
Generalized Kronecker delta contraction. Summing a generalizedKroneckerDelta over one
shared index appended at the end lowers the rank by one and pulls out a factor of card α - n.
This is the reusable combinatorial fact behind all epsilon-epsilon identities.
lemma generalizedKroneckerDelta_sum_snoc {n : ℕ} (μ ν : Fin n → α) :
∑ a : α, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a)
= ((Fintype.card α : ℤ) - n) * generalizedKroneckerDelta μ ν := by α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → α⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
set A : Matrix (Fin n) (Fin n) ℤ :=
Matrix.of fun i j => ((kroneckerDelta (μ i) (ν j) : ℕ) : ℤ) with hA α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
set b : α → Fin n → ℤ := fun a j => ((kroneckerDelta a (ν j) : ℕ) : ℤ) with hb α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
-- Bordering the δ-matrix with the appended index (`Matrix.det_fromBlocks_one₂₂`) and the
-- rank-one update `Matrix.det_add_rankOne` express each summand through row updates of `A`.
have key (a : α) : generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a)
= A.det - ∑ i, ((kroneckerDelta (μ i) a : ℕ) : ℤ) * (A.updateRow i (b a)).det := by
set B : Matrix (Fin n) (Fin 1) ℤ :=
Matrix.of fun i _ => ((kroneckerDelta (μ i) a : ℕ) : ℤ) with hB α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
set C : Matrix (Fin 1) (Fin n) ℤ := Matrix.of fun _ j => b a j with hC α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a j⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
have hblk : (Matrix.of fun (i j : Fin (n + 1)) =>
((kroneckerDelta ((Fin.snoc μ a : Fin (n + 1) → α) i)
((Fin.snoc ν a : Fin (n + 1) → α) j) : ℕ) : ℤ)).submatrix
finSumFinEquiv finSumFinEquiv = Matrix.fromBlocks A B C 1 := by α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → α⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
simp only [← Fin.append_right_eq_snoc μ (fun _ => a), ← Fin.append_right_eq_snoc ν
(fun _ => a)] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a j⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv =
fromBlocks A B C 1 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
ext (i | i) (j | j) inl.inl α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin nj:Fin n⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inl i) (Sum.inl j) =
fromBlocks A B C 1 (Sum.inl i) (Sum.inl j)inl.inr α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin nj:Fin 1⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inl i) (Sum.inr j) =
fromBlocks A B C 1 (Sum.inl i) (Sum.inr j)inr.inl α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin 1j:Fin n⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inr i) (Sum.inl j) =
fromBlocks A B C 1 (Sum.inr i) (Sum.inl j)inr.inr α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin 1j:Fin 1⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inr i) (Sum.inr j) =
fromBlocks A B C 1 (Sum.inr i) (Sum.inr j) α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
· inl.inl α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin nj:Fin n⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inl i) (Sum.inl j) =
fromBlocks A B C 1 (Sum.inl i) (Sum.inl j) α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν simp [hA] All goals completed! 🐙 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
· inl.inr α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin nj:Fin 1⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inl i) (Sum.inr j) =
fromBlocks A B C 1 (Sum.inl i) (Sum.inr j) α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν simp [hB] All goals completed! 🐙 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
· inr.inl α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin 1j:Fin n⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inr i) (Sum.inl j) =
fromBlocks A B C 1 (Sum.inr i) (Sum.inl j) α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν simp [hC, hb] All goals completed! 🐙 α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
· inr.inr α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a ji:Fin 1j:Fin 1⊢ (of fun i j => ↑δ[Fin.append μ (fun x => a) i,Fin.append ν (fun x => a) j]).submatrix (⇑finSumFinEquiv)
(⇑finSumFinEquiv) (Sum.inr i) (Sum.inr j) =
fromBlocks A B C 1 (Sum.inr i) (Sum.inr j) α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν simp [Subsingleton.elim i j] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
have hBC : A - B * C
= A + Matrix.of fun i j => -((kroneckerDelta (μ i) a : ℕ) : ℤ) * b a j := by α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → α⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
ext i j α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1i:Fin nj:Fin n⊢ (A - B * C) i j = (A + of fun i j => -↑δ[μ i,a] * b a j) i j α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
simp [hB, hC, Matrix.mul_apply, sub_eq_add_neg] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
rw [show generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a)
= ((Matrix.of fun (i j : Fin (n + 1)) =>
((kroneckerDelta ((Fin.snoc μ a : Fin (n + 1) → α) i)
((Fin.snoc ν a : Fin (n + 1) → α) j) : ℕ) : ℤ)).submatrix
finSumFinEquiv finSumFinEquiv).det from (Matrix.det_submatrix_equiv_self _ _).symm, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ ((of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv).det =
A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ A.det + ∑ i, -↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
hblk, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ (fromBlocks A B C 1).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ A.det + ∑ i, -↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν Matrix.det_fromBlocks_one₂₂, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ (A - B * C).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ A.det + ∑ i, -↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν hBC, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ (A + of fun i j => -↑δ[μ i,a] * b a j).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ A.det + ∑ i, -↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν Matrix.det_add_rankOne α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ A.det + ∑ i, -↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ A.det + ∑ i, -↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]a:αB:Matrix (Fin n) (Fin 1) ℤ := of fun i x => ↑δ[μ i,a]hB:B = of fun i x => ↑δ[μ i,a]C:Matrix (Fin 1) (Fin n) ℤ := of fun x j => b a jhC:C = of fun x j => b a jhblk:(of fun i j => ↑δ[Fin.snoc μ a i,Fin.snoc ν a j]).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = fromBlocks A B C 1hBC:A - B * C = A + of fun i j => -↑δ[μ i,a] * b a j⊢ A.det + ∑ i, -↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
simp only [neg_mul, Finset.sum_neg_distrib, ← sub_eq_add_neg] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
-- Summing the row updates over the shared index restores `A` itself, once per row.
have hrow (i : Fin n) :
∑ a : α, ((kroneckerDelta (μ i) a : ℕ) : ℤ) * (A.updateRow i (b a)).det = A.det := by
simp_rw [ α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).deti:Fin n⊢ ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν← nsmul_eq_mul, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).deti:Fin n⊢ ∑ x, δ[μ i,x] • (A.updateRow i (b x)).det = A.det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν KroneckerDelta.sum_smul α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).deti:Fin n⊢ (A.updateRow i (b (μ i))).det = A.det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν]
exact congrArg Matrix.det (A.updateRow_eq_self i) α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ a, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν
rw [Finset.sum_congr rfl fun a _ => key a, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ a, (A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).det) = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det Finset.sum_sub_distrib, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ x, A.det - ∑ x, ∑ i, ↑δ[μ i,x] * (A.updateRow i (b x)).det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det Finset.sum_comm, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ x, A.det - ∑ y, ∑ x, ↑δ[μ y,x] * (A.updateRow y (b x)).det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det
Finset.sum_congr rfl fun i _ => hrow i, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ ∑ x, A.det - ∑ i, A.det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det Finset.sum_const, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Finset.univ.card • A.det - ∑ i, A.det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det Finset.sum_const, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Finset.univ.card • A.det - Finset.univ.card • A.det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det
Finset.card_univ, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - Finset.univ.card • A.det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det Finset.card_univ, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - Fintype.card (Fin n) • A.det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det Fintype.card_fin, α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * generalizedKroneckerDelta μ ν α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det
show generalizedKroneckerDelta μ ν = A.det from rfl α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det] α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:ℕμ:Fin n → αν:Fin n → αA:Matrix (Fin n) (Fin n) ℤ := of fun i j => ↑δ[μ i,ν j]hA:A = of fun i j => ↑δ[μ i,ν j]b:α → Fin n → ℤ := fun a j => ↑δ[a,ν j]hb:b = fun a j => ↑δ[a,ν j]key:∀ (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - ∑ i, ↑δ[μ i,a] * (A.updateRow i (b a)).dethrow:∀ (i : Fin n), ∑ a, ↑δ[μ i,a] * (A.updateRow i (b a)).det = A.det⊢ Fintype.card α • A.det - n • A.det = (↑(Fintype.card α) - ↑n) * A.det
simp only [nsmul_eq_mul, ← sub_mul] All goals completed! 🐙
Split a sum over (k+1)-tuples into the last entry and the initial k-tuple.
private lemma sum_over_snoc {X : Type*} [Fintype X] {M : Type*} [AddCommMonoid M] {k : ℕ}
(F : (Fin (k + 1) → X) → M) :
∑ h : Fin (k + 1) → X, F h = ∑ h' : Fin k → X, ∑ c : X, F (Fin.snoc h' c) := by X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ h, F h = ∑ h', ∑ c, F (Fin.snoc h' c)
rw [← Equiv.sum_comp (Fin.snocEquiv (fun _ => X)) F, X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ i, F ((Fin.snocEquiv fun x => X) i) = ∑ h', ∑ c, F (Fin.snoc h' c) X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ y, ∑ x, F ((Fin.snocEquiv fun x => X) (x, y)) = ∑ h', ∑ c, F (Fin.snoc h' c) Fintype.sum_prod_type, X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ x, ∑ y, F ((Fin.snocEquiv fun x => X) (x, y)) = ∑ h', ∑ c, F (Fin.snoc h' c) X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ y, ∑ x, F ((Fin.snocEquiv fun x => X) (x, y)) = ∑ h', ∑ c, F (Fin.snoc h' c) Finset.sum_comm X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ y, ∑ x, F ((Fin.snocEquiv fun x => X) (x, y)) = ∑ h', ∑ c, F (Fin.snoc h' c) X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ y, ∑ x, F ((Fin.snocEquiv fun x => X) (x, y)) = ∑ h', ∑ c, F (Fin.snoc h' c)] X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:ℕF:(Fin (k + 1) → X) → M⊢ ∑ y, ∑ x, F ((Fin.snocEquiv fun x => X) (x, y)) = ∑ h', ∑ c, F (Fin.snoc h' c)
rfl All goals completed! 🐙
Full contraction. Iterating the snoc contraction over all four indices:
∑_f δ^{f}_{f} = 4!. Here f ranges over all maps Fin 4 → Fin 4.
lemma sum_generalizedKroneckerDelta_self (k : ℕ) :
∑ h : Fin k → Fin 4, generalizedKroneckerDelta h h
= ∏ j ∈ Finset.range k, ((4 : ℤ) - j) := by k:ℕ⊢ ∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)
induction k with
| zero => zero ⊢ ∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range 0, (4 - ↑j)
rw [Finset.prod_range_zero, zero ⊢ ∑ h, generalizedKroneckerDelta h h = 1 zero ⊢ generalizedKroneckerDelta default default = 1 Fintype.sum_unique zero ⊢ generalizedKroneckerDelta default default = 1 zero ⊢ generalizedKroneckerDelta default default = 1]zero ⊢ generalizedKroneckerDelta default default = 1
exact Matrix.det_fin_zero All goals completed! 🐙
| succ k ih => succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)⊢ ∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)
rw [sum_over_snoc succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j) succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)]succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)
have hstep : ∀ h' : Fin k → Fin 4, ∑ c : Fin 4,
generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c)
= ((4 : ℤ) - k) * generalizedKroneckerDelta h' h' := by k:ℕ⊢ ∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j) succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)
intro h' k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)h':Fin k → Fin 4⊢ ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)
rw [generalizedKroneckerDelta_sum_snoc h' h', k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)h':Fin k → Fin 4⊢ (↑(Fintype.card (Fin 4)) - ↑k) * generalizedKroneckerDelta h' h' = (4 - ↑k) * generalizedKroneckerDelta h' h' k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)h':Fin k → Fin 4⊢ (↑4 - ↑k) * generalizedKroneckerDelta h' h' = (4 - ↑k) * generalizedKroneckerDelta h' h'succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j) Fintype.card_fin k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)h':Fin k → Fin 4⊢ (↑4 - ↑k) * generalizedKroneckerDelta h' h' = (4 - ↑k) * generalizedKroneckerDelta h' h' k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)h':Fin k → Fin 4⊢ (↑4 - ↑k) * generalizedKroneckerDelta h' h' = (4 - ↑k) * generalizedKroneckerDelta h' h'succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)] k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)h':Fin k → Fin 4⊢ (↑4 - ↑k) * generalizedKroneckerDelta h' h' = (4 - ↑k) * generalizedKroneckerDelta h' h'succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)
push_cast k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)h':Fin k → Fin 4⊢ (4 - ↑k) * generalizedKroneckerDelta h' h' = (4 - ↑k) * generalizedKroneckerDelta h' h'succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)
ringsucc k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)
rw [Finset.sum_congr rfl fun h' _ => hstep h', succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ ∑ h', (4 - ↑k) * generalizedKroneckerDelta h' h' = ∏ j ∈ Finset.range (k + 1), (4 - ↑j) succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∏ j ∈ Finset.range k, (4 - ↑j) = (∏ x ∈ Finset.range k, (4 - ↑x)) * (4 - ↑k) ← Finset.mul_sum, succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∑ i, generalizedKroneckerDelta i i = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∏ j ∈ Finset.range k, (4 - ↑j) = (∏ x ∈ Finset.range k, (4 - ↑x)) * (4 - ↑k) ih, succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∏ j ∈ Finset.range k, (4 - ↑j) = ∏ j ∈ Finset.range (k + 1), (4 - ↑j)succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∏ j ∈ Finset.range k, (4 - ↑j) = (∏ x ∈ Finset.range k, (4 - ↑x)) * (4 - ↑k)
Finset.prod_range_succ succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∏ j ∈ Finset.range k, (4 - ↑j) = (∏ x ∈ Finset.range k, (4 - ↑x)) * (4 - ↑k)succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∏ j ∈ Finset.range k, (4 - ↑j) = (∏ x ∈ Finset.range k, (4 - ↑x)) * (4 - ↑k)]succ k:ℕih:∑ h, generalizedKroneckerDelta h h = ∏ j ∈ Finset.range k, (4 - ↑j)hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - ↑k) * generalizedKroneckerDelta h' h'⊢ (4 - ↑k) * ∏ j ∈ Finset.range k, (4 - ↑j) = (∏ x ∈ Finset.range k, (4 - ↑x)) * (4 - ↑k)
ring All goals completed! 🐙
Single contraction. Contracting the last k of k+1 index pairs leaves one free pair
σ, τ, with the factorial factor (4-1)(4-2)….
lemma sum_generalizedKroneckerDelta_cons (σ τ : Fin 4) (k : ℕ) :
∑ h : Fin k → Fin 4,
generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h)
= (∏ j ∈ Finset.range k, ((3 : ℤ) - j)) * ((kroneckerDelta σ τ : ℕ) : ℤ) := by σ:Fin 4τ:Fin 4k:ℕ⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]
induction k with
| zero => zero σ:Fin 4τ:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range 0, (3 - ↑j)) * ↑δ[σ,τ]
rw [Finset.prod_range_zero, zero σ:Fin 4τ:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = 1 * ↑δ[σ,τ] zero σ:Fin 4τ:Fin 4⊢ generalizedKroneckerDelta (Fin.cons σ default) (Fin.cons τ default) = ↑δ[σ,τ] one_mul, zero σ:Fin 4τ:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = ↑δ[σ,τ] zero σ:Fin 4τ:Fin 4⊢ generalizedKroneckerDelta (Fin.cons σ default) (Fin.cons τ default) = ↑δ[σ,τ] Fintype.sum_unique zero σ:Fin 4τ:Fin 4⊢ generalizedKroneckerDelta (Fin.cons σ default) (Fin.cons τ default) = ↑δ[σ,τ]zero σ:Fin 4τ:Fin 4⊢ generalizedKroneckerDelta (Fin.cons σ default) (Fin.cons τ default) = ↑δ[σ,τ]]zero σ:Fin 4τ:Fin 4⊢ generalizedKroneckerDelta (Fin.cons σ default) (Fin.cons τ default) = ↑δ[σ,τ]
exact Matrix.det_fin_one _ All goals completed! 🐙
| succ k ih => succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
rw [sum_over_snoc succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ] succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]]succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
have hstep : ∀ h' : Fin k → Fin 4, ∑ c : Fin 4,
generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c))
= ((3 : ℤ) - k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') := by σ:Fin 4τ:Fin 4k:ℕ⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ] succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
intro h' σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
rw [Finset.sum_congr rfl fun c _ => by σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) = ?m.133 c σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
rw [Fin.cons_snoc_eq_snoc_cons, σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.snoc (Fin.cons σ h') c) (Fin.cons τ (Fin.snoc h' c)) = ?m.133 c All goals completed! 🐙 σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ] Fin.cons_snoc_eq_snoc_cons σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.snoc (Fin.cons σ h') c) (Fin.snoc (Fin.cons τ h') c) = ?m.133 c All goals completed! 🐙 σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]] All goals completed! 🐙 σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ],
generalizedKroneckerDelta_sum_snoc (Fin.cons σ h') (Fin.cons τ h'), σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑(Fintype.card (Fin 4)) - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ] Fintype.card_fin σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]] σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
push_cast σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]h':Fin k → Fin 4⊢ (4 - (↑k + 1)) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
ringsucc σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', ∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]
rw [Finset.sum_congr rfl fun h' _ => hstep h', succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ ∑ h', (3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h') =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ] succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ((∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]) = (∏ x ∈ Finset.range k, (3 - ↑x)) * (3 - ↑k) * ↑δ[σ,τ] ← Finset.mul_sum, succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ∑ i, generalizedKroneckerDelta (Fin.cons σ i) (Fin.cons τ i) =
(∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ((∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]) = (∏ x ∈ Finset.range k, (3 - ↑x)) * (3 - ↑k) * ↑δ[σ,τ] ih, succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ((∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]) = (∏ j ∈ Finset.range (k + 1), (3 - ↑j)) * ↑δ[σ,τ]succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ((∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]) = (∏ x ∈ Finset.range k, (3 - ↑x)) * (3 - ↑k) * ↑δ[σ,τ]
Finset.prod_range_succ succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ((∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]) = (∏ x ∈ Finset.range k, (3 - ↑x)) * (3 - ↑k) * ↑δ[σ,τ]succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ((∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]) = (∏ x ∈ Finset.range k, (3 - ↑x)) * (3 - ↑k) * ↑δ[σ,τ]]succ σ:Fin 4τ:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) =
(3 - ↑k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')⊢ (3 - ↑k) * ((∏ j ∈ Finset.range k, (3 - ↑j)) * ↑δ[σ,τ]) = (∏ x ∈ Finset.range k, (3 - ↑x)) * (3 - ↑k) * ↑δ[σ,τ]
ring All goals completed! 🐙
Double contraction. Contracting the last k of k+2 index pairs leaves two free pairs,
with value a 2×2 generalized Kronecker delta times the factorial factor.
lemma sum_generalizedKroneckerDelta_cons₂ (ρ σ τ ω : Fin 4) (k : ℕ) :
∑ h : Fin k → Fin 4,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h))
= (∏ j ∈ Finset.range k, ((2 : ℤ) - j))
* generalizedKroneckerDelta ![ρ, σ] ![τ, ω] := by ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕ⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
induction k with
| zero => zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range 0, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
rw [Finset.prod_range_zero, zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
1 * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω] one_mul, zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω] zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω] Fintype.sum_unique zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]]zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
have e1 : ∀ d : Fin 0 → Fin 4, (Fin.cons ρ (Fin.cons σ d) : Fin 2 → Fin 4) = ![ρ, σ] := by ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕ⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
intro d ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4d:Fin 0 → Fin 4⊢ Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]; funext i ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4d:Fin 0 → Fin 4i:Fin (1 + 1)⊢ Fin.cons ρ (Fin.cons σ d) i = ![ρ, σ] izero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]; fin_cases i «0» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4d:Fin 0 → Fin 4⊢ Fin.cons ρ (Fin.cons σ d) ((fun i => i) ⟨0, ⋯⟩) = ![ρ, σ] ((fun i => i) ⟨0, ⋯⟩)«1» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4d:Fin 0 → Fin 4⊢ Fin.cons ρ (Fin.cons σ d) ((fun i => i) ⟨1, ⋯⟩) = ![ρ, σ] ((fun i => i) ⟨1, ⋯⟩)zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω] <;> «0» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4d:Fin 0 → Fin 4⊢ Fin.cons ρ (Fin.cons σ d) ((fun i => i) ⟨0, ⋯⟩) = ![ρ, σ] ((fun i => i) ⟨0, ⋯⟩)«1» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4d:Fin 0 → Fin 4⊢ Fin.cons ρ (Fin.cons σ d) ((fun i => i) ⟨1, ⋯⟩) = ![ρ, σ] ((fun i => i) ⟨1, ⋯⟩)zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω] rflzero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
have e2 : ∀ d : Fin 0 → Fin 4, (Fin.cons τ (Fin.cons ω d) : Fin 2 → Fin 4) = ![τ, ω] := by ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕ⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
intro d ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]d:Fin 0 → Fin 4⊢ Fin.cons τ (Fin.cons ω d) = ![τ, ω]zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]; funext i ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]d:Fin 0 → Fin 4i:Fin (1 + 1)⊢ Fin.cons τ (Fin.cons ω d) i = ![τ, ω] izero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]; fin_cases i «0» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]d:Fin 0 → Fin 4⊢ Fin.cons τ (Fin.cons ω d) ((fun i => i) ⟨0, ⋯⟩) = ![τ, ω] ((fun i => i) ⟨0, ⋯⟩)«1» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]d:Fin 0 → Fin 4⊢ Fin.cons τ (Fin.cons ω d) ((fun i => i) ⟨1, ⋯⟩) = ![τ, ω] ((fun i => i) ⟨1, ⋯⟩)zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω] <;> «0» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]d:Fin 0 → Fin 4⊢ Fin.cons τ (Fin.cons ω d) ((fun i => i) ⟨0, ⋯⟩) = ![τ, ω] ((fun i => i) ⟨0, ⋯⟩)«1» ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]d:Fin 0 → Fin 4⊢ Fin.cons τ (Fin.cons ω d) ((fun i => i) ⟨1, ⋯⟩) = ![τ, ω] ((fun i => i) ⟨1, ⋯⟩)zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω] rflzero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ default)) (Fin.cons τ (Fin.cons ω default)) =
generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
rw [e1, zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta ![ρ, σ] (Fin.cons τ (Fin.cons ω default)) = generalizedKroneckerDelta ![ρ, σ] ![τ, ω] All goals completed! 🐙 e2 zero ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4e1:∀ (d : Fin 0 → Fin 4), Fin.cons ρ (Fin.cons σ d) = ![ρ, σ]e2:∀ (d : Fin 0 → Fin 4), Fin.cons τ (Fin.cons ω d) = ![τ, ω]⊢ generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = generalizedKroneckerDelta ![ρ, σ] ![τ, ω] All goals completed! 🐙] All goals completed! 🐙
| succ k ih => succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
rw [sum_over_snoc succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]]succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
have hstep : ∀ h' : Fin k → Fin 4, ∑ c : Fin 4,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c)))
(Fin.cons τ (Fin.cons ω (Fin.snoc h' c)))
= ((2 : ℤ) - k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h'))
(Fin.cons τ (Fin.cons ω h')) := by ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕ⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
intro h' ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ ∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
rw [Finset.sum_congr rfl fun c _ => by ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) = ?m.717 c ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
rw [Fin.cons_snoc_eq_snoc_cons, ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.cons ρ (Fin.snoc (Fin.cons σ h') c)) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) = ?m.717 c All goals completed! 🐙 ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] Fin.cons_snoc_eq_snoc_cons, ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.snoc (Fin.cons ρ (Fin.cons σ h')) c) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) = ?m.717 c All goals completed! 🐙 ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
Fin.cons_snoc_eq_snoc_cons, ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.snoc (Fin.cons ρ (Fin.cons σ h')) c) (Fin.cons τ (Fin.snoc (Fin.cons ω h') c)) = ?m.717 c All goals completed! 🐙 ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] Fin.cons_snoc_eq_snoc_cons ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4c:Fin 4x✝:c ∈ Finset.univ⊢ generalizedKroneckerDelta (Fin.snoc (Fin.cons ρ (Fin.cons σ h')) c) (Fin.snoc (Fin.cons τ (Fin.cons ω h')) c) = ?m.717 c All goals completed! 🐙 ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]] All goals completed! 🐙 ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω],
generalizedKroneckerDelta_sum_snoc (Fin.cons ρ (Fin.cons σ h'))
(Fin.cons τ (Fin.cons ω h')), ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑(Fintype.card (Fin 4)) - ↑(k + 1 + 1)) *
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] Fintype.card_fin ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (↑4 - ↑(k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
push_cast ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]h':Fin k → Fin 4⊢ (4 - (↑k + 1 + 1)) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
ringsucc ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h',
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
rw [Finset.sum_congr rfl fun h' _ => hstep h', succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ ∑ h', (2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h')) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ((∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) =
(∏ x ∈ Finset.range k, (2 - ↑x)) * (2 - ↑k) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] ← Finset.mul_sum, succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ∑ i, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ i)) (Fin.cons τ (Fin.cons ω i)) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ((∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) =
(∏ x ∈ Finset.range k, (2 - ↑x)) * (2 - ↑k) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] ih, succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ((∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) =
(∏ j ∈ Finset.range (k + 1), (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ((∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) =
(∏ x ∈ Finset.range k, (2 - ↑x)) * (2 - ↑k) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
Finset.prod_range_succ succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ((∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) =
(∏ x ∈ Finset.range k, (2 - ↑x)) * (2 - ↑k) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ((∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) =
(∏ x ∈ Finset.range k, (2 - ↑x)) * (2 - ↑k) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]]succ ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ℕih:∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
(∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep:∀ (h' : Fin k → Fin 4),
∑ c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) =
(2 - ↑k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))⊢ (2 - ↑k) * ((∏ j ∈ Finset.range k, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) =
(∏ x ∈ Finset.range k, (2 - ↑x)) * (2 - ↑k) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
ring All goals completed! 🐙
Symbol-level full contraction over Fin 4 → Fin 4.
lemma sum_generalizedKroneckerDelta_mul_self :
∑ g : Fin 4 → Fin 4,
generalizedKroneckerDelta g id * generalizedKroneckerDelta g id = (24 : ℤ) := by ⊢ ∑ g, generalizedKroneckerDelta g id * generalizedKroneckerDelta g id = 24
rw [Finset.sum_congr rfl fun g _ => generalizedKroneckerDelta_mul g g, ⊢ ∑ g, generalizedKroneckerDelta g g = 24 ⊢ ∏ j ∈ Finset.range 4, (4 - ↑j) = 24
sum_generalizedKroneckerDelta_self 4 ⊢ ∏ j ∈ Finset.range 4, (4 - ↑j) = 24 ⊢ ∏ j ∈ Finset.range 4, (4 - ↑j) = 24] ⊢ ∏ j ∈ Finset.range 4, (4 - ↑j) = 24
norm_num [Finset.prod_range_succ] All goals completed! 🐙
Symbol-level triple contraction, one free pair σ, τ.
lemma sum_generalizedKroneckerDelta_mul_cons (σ τ : Fin 4) :
∑ h : Fin 3 → Fin 4,
generalizedKroneckerDelta (Fin.cons σ h) id
* generalizedKroneckerDelta (Fin.cons τ h) id
= 6 * ((kroneckerDelta σ τ : ℕ) : ℤ) := by σ:Fin 4τ:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) id * generalizedKroneckerDelta (Fin.cons τ h) id = 6 * ↑δ[σ,τ]
rw [Finset.sum_congr rfl fun h _ =>
generalizedKroneckerDelta_mul (Fin.cons σ h) (Fin.cons τ h), σ:Fin 4τ:Fin 4⊢ ∑ h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = 6 * ↑δ[σ,τ] σ:Fin 4τ:Fin 4⊢ (∏ j ∈ Finset.range 3, (3 - ↑j)) * ↑δ[σ,τ] = 6 * ↑δ[σ,τ]
sum_generalizedKroneckerDelta_cons σ τ 3 σ:Fin 4τ:Fin 4⊢ (∏ j ∈ Finset.range 3, (3 - ↑j)) * ↑δ[σ,τ] = 6 * ↑δ[σ,τ] σ:Fin 4τ:Fin 4⊢ (∏ j ∈ Finset.range 3, (3 - ↑j)) * ↑δ[σ,τ] = 6 * ↑δ[σ,τ]] σ:Fin 4τ:Fin 4⊢ (∏ j ∈ Finset.range 3, (3 - ↑j)) * ↑δ[σ,τ] = 6 * ↑δ[σ,τ]
norm_num [Finset.prod_range_succ] All goals completed! 🐙Symbol-level double contraction, two free pairs.
lemma sum_generalizedKroneckerDelta_mul_cons₂ (ρ σ τ ω : Fin 4) :
∑ h : Fin 2 → Fin 4,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) id
* generalizedKroneckerDelta (Fin.cons τ (Fin.cons ω h)) id
= 2 * (((kroneckerDelta ρ τ : ℕ) : ℤ) * ((kroneckerDelta σ ω : ℕ) : ℤ)
- ((kroneckerDelta ρ ω : ℕ) : ℤ) * ((kroneckerDelta σ τ : ℕ) : ℤ)) := by ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ ∑ h,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) id *
generalizedKroneckerDelta (Fin.cons τ (Fin.cons ω h)) id =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])
have hdet : generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
= ((kroneckerDelta ρ τ : ℕ) : ℤ) * ((kroneckerDelta σ ω : ℕ) : ℤ)
- ((kroneckerDelta ρ ω : ℕ) : ℤ) * ((kroneckerDelta σ τ : ℕ) : ℤ) := by
rw [show generalizedKroneckerDelta ![ρ, σ] ![τ, ω]
= (Matrix.of fun i j => ((kroneckerDelta (![ρ, σ] i) (![τ, ω] j) : ℕ) : ℤ)).det from rfl, ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ (of fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]).det = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 0 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 1 -
of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 1 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 0 =
↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ ∑ h,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) id *
generalizedKroneckerDelta (Fin.cons τ (Fin.cons ω h)) id =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])
Matrix.det_fin_two ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 0 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 1 -
of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 1 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 0 =
↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 0 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 1 -
of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 1 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 0 =
↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ ∑ h,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) id *
generalizedKroneckerDelta (Fin.cons τ (Fin.cons ω h)) id =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4⊢ of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 0 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 1 -
of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 0 1 * of (fun i j => ↑δ[![ρ, σ] i,![τ, ω] j]) 1 0 =
↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ ∑ h,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) id *
generalizedKroneckerDelta (Fin.cons τ (Fin.cons ω h)) id =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])
simp ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ ∑ h,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) id *
generalizedKroneckerDelta (Fin.cons τ (Fin.cons ω h)) id =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ ∑ h,
generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) id *
generalizedKroneckerDelta (Fin.cons τ (Fin.cons ω h)) id =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])
rw [Finset.sum_congr rfl fun h _ =>
generalizedKroneckerDelta_mul (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)), ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ ∑ h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ (∏ j ∈ Finset.range 2, (2 - ↑j)) * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) = 2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])
sum_generalizedKroneckerDelta_cons₂ ρ σ τ ω 2, ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ (∏ j ∈ Finset.range 2, (2 - ↑j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] =
2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ (∏ j ∈ Finset.range 2, (2 - ↑j)) * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) = 2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) hdet ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ (∏ j ∈ Finset.range 2, (2 - ↑j)) * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) = 2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ (∏ j ∈ Finset.range 2, (2 - ↑j)) * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) = 2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])] ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = ↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]⊢ (∏ j ∈ Finset.range 2, (2 - ↑j)) * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ]) = 2 * (↑δ[ρ,τ] * ↑δ[σ,ω] - ↑δ[ρ,ω] * ↑δ[σ,τ])
norm_num [Finset.prod_range_succ] All goals completed! 🐙