From f9a4fec08ce9069725170dd403e0344ee60d5cc9 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Tue, 16 Jun 2026 15:42:21 -0500 Subject: [PATCH 1/8] feat: generalized Kronecker delta definition --- Physlib/Mathematics/KroneckerDelta.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index a5b23d9f8..14f283307 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -131,4 +131,24 @@ lemma finset_sum_sum_smul_eq_zero {s s' : Finset α} {f : α → α → M} end Sums +/-! + +# Generalized Kronecker delta + +-/ + +section Generalized +open Matrix + +/-- Integer-valued Kronecker entry via the existing `kroneckerDelta`. -/ +local notation "δℤ" => (fun ρ σ => ((kroneckerDelta ρ σ : ℕ) : ℤ)) + +/-- Generalized Kronecker delta: +`δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. -/ +def generalizedKroneckerDelta (n : ℕ) (d : ℕ := 3) + (μ : Fin n → Fin (d + 1)) (ν : Fin n → Fin (d + 1)) : ℤ := + Matrix.det (fun i j => δℤ (μ i) (ν j)) + +end Generalized + end KroneckerDelta From dcc631aba47046be011c7b0ee421c2e272e5a359 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Tue, 16 Jun 2026 18:13:26 -0500 Subject: [PATCH 2/8] fix: allow any finite type for generalizedKroneckerDelta indices --- Physlib/Mathematics/KroneckerDelta.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index 14f283307..e56dfe0ac 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -144,9 +144,11 @@ open Matrix local notation "δℤ" => (fun ρ σ => ((kroneckerDelta ρ σ : ℕ) : ℤ)) /-- Generalized Kronecker delta: -`δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. -/ -def generalizedKroneckerDelta (n : ℕ) (d : ℕ := 3) - (μ : Fin n → Fin (d + 1)) (ν : Fin n → Fin (d + 1)) : ℤ := +`δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. + +This is defined for any finite type `α` with decidable equality. -/ +def generalizedKroneckerDelta {α : Type} [DecidableEq α] [Fintype α] (n : ℕ) + (μ : Fin n → α) (ν : Fin n → α) : ℤ := Matrix.det (fun i j => δℤ (μ i) (ν j)) end Generalized From b4240e7d030db8a9dd50d254f9a4e71a2f337623 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Wed, 17 Jun 2026 08:07:50 -0500 Subject: [PATCH 3/8] fix: style Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> --- Physlib/Mathematics/KroneckerDelta.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index e56dfe0ac..97e4569ed 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -144,7 +144,7 @@ open Matrix local notation "δℤ" => (fun ρ σ => ((kroneckerDelta ρ σ : ℕ) : ℤ)) /-- Generalized Kronecker delta: -`δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. +`δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. This is defined for any finite type `α` with decidable equality. -/ def generalizedKroneckerDelta {α : Type} [DecidableEq α] [Fintype α] (n : ℕ) From 080816e6e35339ddd7897076f9049b7c9795f6e7 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Wed, 17 Jun 2026 08:10:33 -0500 Subject: [PATCH 4/8] feat: use more generic index domain type Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> --- Physlib/Mathematics/KroneckerDelta.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index 97e4569ed..303ff96e1 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -147,8 +147,9 @@ local notation "δℤ" => (fun ρ σ => ((kroneckerDelta ρ σ : ℕ) : ℤ)) `δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. This is defined for any finite type `α` with decidable equality. -/ -def generalizedKroneckerDelta {α : Type} [DecidableEq α] [Fintype α] (n : ℕ) - (μ : Fin n → α) (ν : Fin n → α) : ℤ := +def generalizedKroneckerDelta {α ι : Type} [DecidableEq α] [Fintype α] + [DecidableEq ι] [Fintype ι] + (μ : ι → α) (ν : ι → α) : ℤ := Matrix.det (fun i j => δℤ (μ i) (ν j)) end Generalized From c13394f3972e9e9e796f41ac71ff90b65854c017 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Wed, 17 Jun 2026 08:25:02 -0500 Subject: [PATCH 5/8] fix: style --- Physlib/Mathematics/KroneckerDelta.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index 303ff96e1..ce73154ab 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -147,8 +147,8 @@ local notation "δℤ" => (fun ρ σ => ((kroneckerDelta ρ σ : ℕ) : ℤ)) `δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. This is defined for any finite type `α` with decidable equality. -/ -def generalizedKroneckerDelta {α ι : Type} [DecidableEq α] [Fintype α] - [DecidableEq ι] [Fintype ι] +def generalizedKroneckerDelta {α ι : Type} [DecidableEq α] [Fintype α] + [DecidableEq ι] [Fintype ι] (μ : ι → α) (ν : ι → α) : ℤ := Matrix.det (fun i j => δℤ (μ i) (ν j)) From fe07058ebe1aacf9b88b069053d488655ba7f594 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Wed, 17 Jun 2026 10:49:23 -0500 Subject: [PATCH 6/8] fix: import determinant --- Physlib/Mathematics/KroneckerDelta.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index ce73154ab..79c0487ce 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise public import Mathlib.Algebra.CharZero.Defs public import Mathlib.Algebra.Field.Defs public import Mathlib.Algebra.Module.Defs +public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic /-! # Kronecker delta From 1dcd5cbdd590a1cb7e19b2265d8b43fae43cdae1 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Wed, 17 Jun 2026 12:14:00 -0500 Subject: [PATCH 7/8] =?UTF-8?q?fix:=20rm=20Fintype=20=CE=B1=20from=20gener?= =?UTF-8?q?alizedKroneckerDelta?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Physlib/Mathematics/KroneckerDelta.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index 79c0487ce..24fe3699a 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -148,7 +148,7 @@ local notation "δℤ" => (fun ρ σ => ((kroneckerDelta ρ σ : ℕ) : ℤ)) `δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`. This is defined for any finite type `α` with decidable equality. -/ -def generalizedKroneckerDelta {α ι : Type} [DecidableEq α] [Fintype α] +def generalizedKroneckerDelta {α ι : Type} [DecidableEq α] [DecidableEq ι] [Fintype ι] (μ : ι → α) (ν : ι → α) : ℤ := Matrix.det (fun i j => δℤ (μ i) (ν j)) From 2c6bc228cb61e5af87e0e57199c9177f4e6e0c72 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Thu, 18 Jun 2026 08:18:41 -0500 Subject: [PATCH 8/8] fix: address unusedSimpArgs warnings --- Physlib/Mathematics/KroneckerDelta.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Physlib/Mathematics/KroneckerDelta.lean b/Physlib/Mathematics/KroneckerDelta.lean index 24fe3699a..4420a2c25 100644 --- a/Physlib/Mathematics/KroneckerDelta.lean +++ b/Physlib/Mathematics/KroneckerDelta.lean @@ -57,7 +57,7 @@ lemma smul_of_eq_zero [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i lemma smul_eq_zero_iff [AddMonoid M] (i j : α) (f : α → α → M) : δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0 := by rcases eq_or_ne i j with (rfl | hne) - · simp [one_nsmul] + · simp · simp [eq_zero_of_ne, hne] lemma smul_eq_zero_iff' [AddMonoid M] (i : α) (f : α → α → M) : @@ -83,7 +83,7 @@ lemma smul_symm [AddMonoid M] (i j : α) (f : α → α → M) : δ[i,j] • f j lemma symmetrize [AddMonoid M] (i j : α) (f : α → α → M) : δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j := by rcases eq_or_ne i j with (rfl | hne) - · simp [one_nsmul, two_nsmul] + · simp [two_nsmul] · simp [eq_zero_of_ne hne] lemma symmetrize' [AddCommMonoid M] {K : Type*} [Semifield K] [CharZero K] [Module K M] @@ -114,7 +114,7 @@ lemma sum_mul [Fintype α] (i j : α) : ∑ k : α, δ[i,k] * δ[k,j] = δ[i,j] @[simp] lemma sum_smul [Fintype α] (i : α) (f : α → M) : ∑ j : α, δ[i,j] • f j = f i := by - simp [kroneckerDelta, one_nsmul] + simp [kroneckerDelta] lemma sum_sum_smul_eq_zero [Fintype α] {f : α → α → M} (hf : ∀ i : α, f i i = 0) : ∑ i : α, ∑ j : α, δ[i,j] • f i j = 0 := by @@ -122,7 +122,7 @@ lemma sum_sum_smul_eq_zero [Fintype α] {f : α → α → M} (hf : ∀ i : α, lemma finset_sum_smul (s : Finset α) (i : α) (f : α → M) : ∑ j ∈ s, δ[i,j] • f j = if i ∈ s then f i else 0 := by - simp [kroneckerDelta, one_nsmul] + simp [kroneckerDelta] lemma finset_sum_sum_smul_eq_zero {s s' : Finset α} {f : α → α → M} (hf : ∀ i ∈ s ∩ s', f i i = 0) : ∑ i ∈ s, ∑ j ∈ s', δ[i,j] • f i j = 0 := by