feat: Kronecker delta api

[gloges]

Introduces a basic api for the Kronecker delta function.

• I've kept to lemmas which adhere to the Einstein summation rules that indices occur at most twice in each term and free indices match across = (unless one side is zero). Hence no δ[i,j] • f i j = δ[i,j] • f i i lemma.
• Commutators.lean and LaplaceRungeLenzVector.lean required some fixes, which I have done crudely (w/ sorries for some of the more computation-heavy lemmas); I will revisit these soon.

[morrison-daniel]

Just a few style points for now, I'll take a deeper look soon.

[gloges]

I've cleaned up the lemma names and added (double) sums over finite subsets. After the merge, needed to add @[expose] public section to fix some errors.

[zhikaip]

You could remove the awaiting author and merge-conflict tags to let the reviewers know when the PR is ready