Commit graph

1545 commits

Author SHA1 Message Date
jstoobysmith
c86974a617 refactor: Rename OperatorAlgebra 2025-01-22 08:53:08 +00:00
Joseph Tooby-Smith
7b396501e7
docs: Update website (#288)
* Create WebsiteInstructions.md

* Update index.markdown
2025-01-22 07:46:47 +00:00
jstoobysmith
4ca4eac8c5 refactor: Uncontracted List organization 2025-01-22 06:48:58 +00:00
jstoobysmith
27cbb03275 refactor: Normal order results 2025-01-22 06:26:28 +00:00
jstoobysmith
509d536577 refactor: Organize supercommute for CrAnAlgebra 2025-01-22 05:51:52 +00:00
Joseph Tooby-Smith
2fcafb1796
Docs: Documentation related to Wick contraction (#287)
* refactor: Fix field struct defn.

* rename: FieldStruct to FieldSpecification

* feat: Add examples of field specifications

* docs: Slight improvement of module docs

* refactor: Rename CreateAnnihilate

* docs: Algebras

* Update CrAnStates.lean
2025-01-21 10:23:05 +00:00
Joseph Tooby-Smith
b5c987180a
refactor: Some properties of field specifications (#285)
* refactor: Fix field struct defn.

* rename: FieldStruct to FieldSpecification

* feat: Add examples of field specifications

* docs: Slight improvement of module docs
2025-01-21 06:11:47 +00:00
Joseph Tooby-Smith
bb1db930b5
refactor: Fix field struct defn. (#284) 2025-01-20 16:16:09 +00:00
Joseph Tooby-Smith
17f84b7153
feat: Time dependent Wick theorem. (#274)
feat: Proof of the time-dependent Wick's theorem
2025-01-20 15:17:48 +00:00
Joseph Tooby-Smith
4d43698b3c
Merge pull request #283 from HEPLean/jstoobysmith-patch-1
Update README.md
2025-01-20 09:01:12 +00:00
Joseph Tooby-Smith
5fafa11296
Update README.md 2025-01-20 08:37:24 +00:00
KUO-TSAN HSU (Gordon)
656a3e422f
chore: bump toolchain to v4.15.0
#281 adapt code to v4.15.0 and fix long heartbeats, e.g., toDualRep_apply_eq_contrOneTwoLeft.

---------

Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
2025-01-20 15:42:53 +08:00
Joseph Tooby-Smith
6e31281a5b
Merge pull request #280 from HEPLean/fix-workflows
chore: Fix workflow
2025-01-17 10:56:25 +00:00
jstoobysmith
4f0a1b5944 Update docs.yml 2025-01-17 10:26:22 +00:00
jstoobysmith
20bd9340ce Update docs.yml 2025-01-17 09:43:58 +00:00
jstoobysmith
470ba76879 Update docs.yml 2025-01-17 07:04:24 +00:00
jstoobysmith
986d7ef3bd Update docs.yml 2025-01-17 07:03:09 +00:00
Joseph Tooby-Smith
5e4893c8a5
Merge pull request #279 from HEPLean/fix-typos
fix typos
2025-01-16 16:05:32 +00:00
Pietro Monticone
7b8a6f6ce6 fix typos 2025-01-16 11:28:08 +01:00
Joseph Tooby-Smith
6455509585
Merge pull request #278 from HEPLean/pitmonticone/fix-typos
fix typos
2025-01-14 09:49:15 +00:00
Pietro Monticone
f896988894 clean Lorentz 2025-01-14 01:29:44 +01:00
Pietro Monticone
ebde396335 clean PT 2025-01-14 00:11:36 +01:00
Pietro Monticone
f1075ef57e clean meta 2025-01-14 00:11:25 +01:00
Pietro Monticone
d911b3b0f9 clean mathematics 2025-01-14 00:11:17 +01:00
Pietro Monticone
fa425ef606 Update CreateAnnihilateSection.lean 2025-01-14 00:00:39 +01:00
Pietro Monticone
8bcc691bdf Update CreateAnnihilateSect.lean 2025-01-14 00:00:37 +01:00
Pietro Monticone
89baced65e cleanup 2025-01-13 23:59:30 +01:00
Pietro Monticone
19cb08e05b clean Tensors 2025-01-13 23:49:47 +01:00
Pietro Monticone
dbc1a3e046 Update ProdAssoc.lean 2025-01-13 23:07:58 +01:00
Pietro Monticone
4eca44a404 Update PermContr.lean 2025-01-13 23:07:55 +01:00
Pietro Monticone
af72d87449 Update ContrContr.lean 2025-01-13 23:07:53 +01:00
Pietro Monticone
5cfdf5358c Update Basic.lean 2025-01-13 23:07:51 +01:00
Pietro Monticone
76860012f7 Update Elab.lean 2025-01-13 23:07:49 +01:00
Pietro Monticone
206c9fa73f Update Basic.lean 2025-01-13 23:07:46 +01:00
Pietro Monticone
eca8be8bab fix typos 2025-01-13 22:52:18 +01:00
Joseph Tooby-Smith
059e8fe464
Merge pull request #276 from kuotsanhsu/toLorentzGroup_det_one
Implement toLorentzGroup_det_one
2025-01-13 09:33:13 +00:00
jstoobysmith
7110a07299 refactor: Moved module doc string 2025-01-12 17:11:04 +00:00
kuotsanhsu
6d47ea18a0 refactor: add module docstrings, add copyright headers, and fix other typos 2025-01-12 19:40:15 +08:00
jstoobysmith
4fa4a28d5d refactor: Lint 2025-01-11 17:11:38 +00:00
kuotsanhsu
6a3bb431bf refactor: Lint style 2025-01-11 21:24:54 +08:00
kuotsanhsu
1053ccaa3a refactor: Define Equiv.finAddEquivSigmaCond using existing definitions from Mathlib 2025-01-11 21:24:32 +08:00
jstoobysmith
b37bfc0748 Update build.yml 2025-01-10 16:15:15 +00:00
jstoobysmith
90e5ab2741 Update build.yml 2025-01-10 16:03:08 +00:00
jstoobysmith
ca133be5ba Update build.yml 2025-01-10 15:59:31 +00:00
kuotsanhsu
0297f0e288 feat: toLorentzGroup_det_one 2025-01-10 23:14:44 +08:00
kuotsanhsu
5baa184092 feat: schur_triangulation 2025-01-10 23:12:16 +08:00
Joseph Tooby-Smith
daa0f5f7ff
Merge pull request #275 from HEPLean/Website-update
refactor: Update website url
2025-01-08 16:14:22 +00:00
jstoobysmith
f3a7a1e694 Update _config.yml 2025-01-08 15:56:29 +00:00
Joseph Tooby-Smith
acea86ee08
Merge pull request #273 from HEPLean/WickContract
feat: Field struct and creation and annihilation sections
2025-01-06 12:25:30 +00:00
jstoobysmith
f1cbb2fe4d refactor: Lint 2025-01-06 11:46:59 +00:00