feat(Relativity): epsilon-epsilon contraction identities for the Levi-Civita tensor - #1335

Merged

jstoobysmith merged 7 commits into

leanprover-community:masterfrom

Robby955:feat/levicivita-epsilon-contractions

Jul 6, 2026

Commits on Jul 1, 2026

feat(Relativity): add Levi-Civita epsilon-epsilon contraction identities
Robby955
committed
9c9adc3
fix(Relativity): address review of Levi-Civita contraction identities
Robby955
committed
7ddc53f

Commits on Jul 4, 2026

refactor(Mathematics): move combinatorial Levi-Civita contraction lemmas out of Relativity
Robby955
committed
f8d6fd1
refactor(Mathematics): move KroneckerDelta into a directory, unwrap contraction namespace
Robby955
committed
13f5811
docs(Relativity): frame Levi-Civita contractions as Euclidean, add Lorentz TODO, fix lints
Robby955
committed
360642e

Commits on Jul 5, 2026

update: TODO statment
jstoobysmith
committed
13edc2d
refactor: Update with Euclidean
jstoobysmith
committed
1dd9e4a