DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #298 from HEPLean/FieldOpAlgebra

Browse source 
feat: Add FieldOpAlgebra
This commit is contained in:
Joseph Tooby-Smith 2025-01-27 06:40:56 +00:00 • committed by GitHub
commit 0dfb2b725d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 389 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/Lorentz/ComplexTensor/Basis.lean
View file

@ -48,7 +48,6 @@ lemma perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
simp only [Functor.const_obj_obj, OverColor.mk_hom] at h1
rw [h1]
TODO "Generalize `basis_eq_FD`."
lemma basis_eq_FD {n : ℕ} (c : Fin n → complexLorentzTensor.C)
(b : Π j, Fin (complexLorentzTensor.repDim (c j))) (i : Fin n)
(h : { as := c i } = { as := c1 }) :