Commit graph

1518 commits

Author SHA1 Message Date
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
jstoobysmith
fb31135426 feat: Field struct and creation and annihilation sections 2025-01-06 10:45:50 +00:00
Joseph Tooby-Smith
7756364acb
Merge pull request #272 from HEPLean/WickContract
Relation between Wick contractions and involutions, and the cardinality of full Wick contractions.
2025-01-06 05:55:28 +00:00
jstoobysmith
83908c6d0d refactor: Lint and update involutions of Fin n 2025-01-06 05:35:35 +00:00
jstoobysmith
408a676bbd refactor: style lint 2025-01-05 17:00:36 +00:00
jstoobysmith
7026d8ce66 refactor: free simps 2025-01-05 16:46:15 +00:00
jstoobysmith
9184f6087c feat: Update free simp 2025-01-05 16:00:30 +00:00
jstoobysmith
1ab0c6f769 feat: Cardinality of involutions and refactor 2025-01-05 13:07:32 +00:00
jstoobysmith
840d16a581 feat: number of full contractions 2025-01-04 14:22:58 +00:00
jstoobysmith
eadb354477 feat: equivalence between involutions and contractions 2025-01-04 11:56:26 +00:00
jstoobysmith
7d1f15e18a feat: Contractions and involutions 2025-01-03 15:13:16 +00:00
Joseph Tooby-Smith
508850fd4e
Merge pull request #271 from HEPLean/WickContract
refactor: renaming variables and golfing
2025-01-03 05:31:37 +00:00
jstoobysmith
bab9f10763 refactor: basic golfing and renaming 2025-01-03 05:12:54 +00:00
jstoobysmith
dcfc4b1318 refactor: Remove super algebra file 2024-12-22 09:55:56 +00:00
Joseph Tooby-Smith
abfda8fd16
Merge pull request #270 from HEPLean/WickContract
refactor: Remove redundant imports
2024-12-20 20:57:08 +00:00
jstoobysmith
2e5b66655e refactor: Remove rest of redundant imports 2024-12-20 17:05:08 +00:00
jstoobysmith
14677e6332 refactor: More redundant imports 2024-12-20 16:53:14 +00:00
jstoobysmith
f3cb311028 refactor: Remove redundent imports 2024-12-20 16:46:11 +00:00
Joseph Tooby-Smith
33dca6e003
Merge pull request #269 from HEPLean/WickContract
refactor: Move contractions
2024-12-20 16:29:55 +00:00
jstoobysmith
5bcf3b3962 feat: Add contraction involution file 2024-12-20 15:42:35 +00:00
jstoobysmith
968d8ab94b refactor: Move contractions 2024-12-20 15:21:13 +00:00
Joseph Tooby-Smith
fee2852367
Merge pull request #268 from HEPLean/WickContract
feat: Introduce field statistics
2024-12-20 14:37:43 +00:00
jstoobysmith
b454a7e23c refactor: Lint 2024-12-20 14:07:20 +00:00
jstoobysmith
d28b673057 refactor: Update operator map 2024-12-20 14:05:27 +00:00
jstoobysmith
da595e8ad2 reactor: Fix spelling 2024-12-20 13:57:29 +00:00
jstoobysmith
b93ae33963 refactor: Update contractions 2024-12-20 13:53:22 +00:00
jstoobysmith
e4dafbd291 refactor: Lint 2024-12-20 13:34:49 +00:00
jstoobysmith
a5e0f3ceac refactor: building version 2024-12-20 13:33:39 +00:00