Docs: Index notation

2024-08-15 12:39:52 -04:00 · 2024-08-15 12:39:52 -04:00 · a44db0c3c0
commit a44db0c3c0
parent 02ff4f0fdb
8 changed files with 144 additions and 36 deletions
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean
@ -9,6 +9,11 @@ import Mathlib.Algebra.Order.Ring.Nat

 # withDuals equal to withUniqueDuals

+In a permissible list of indices every index which has a dual has a unique dual.
+This corresponds to the condition that `l.withDual = l.withUniqueDual`.
+
+We prove lemmas relating to this condition.
+
 -/

 namespace IndexNotation