Commit graph

54 commits

Author SHA1 Message Date
jstoobysmith
5218db3591 feat: Normalize index list 2024-08-30 07:08:05 -04:00
jstoobysmith
c5ba841f5d refactor: Lint 2024-08-28 14:53:38 -04:00
jstoobysmith
44c8cce2bc refactor: Lint 2024-08-28 14:48:22 -04:00
jstoobysmith
b96e437c45 refactor: version which builds 2024-08-28 14:35:01 -04:00
jstoobysmith
47d639bb1a refactor: Index notation 2024-08-28 14:16:51 -04:00
jstoobysmith
6b0ecc4405 refactor: index notation 2024-08-26 15:23:38 -04:00
jstoobysmith
4f9b572274 refactor: Lint 2024-08-26 10:11:49 -04:00
jstoobysmith
201ae42db8 feat: Add append contract 2024-08-26 10:05:39 -04:00
jstoobysmith
d04874c40f feat: AppendCond contr 2024-08-26 09:31:40 -04:00
jstoobysmith
828aecd1fd refactor: Lint 2024-08-26 06:28:14 -04:00
jstoobysmith
ebb9fcdde2 refactor: countPCond 2024-08-26 06:20:08 -04:00
jstoobysmith
d56444a0c1 refactor: Lint 2024-08-26 06:00:22 -04:00
jstoobysmith
6d81fc2fd8 refactor: More countId 2024-08-26 05:57:00 -04:00
jstoobysmith
10e796a007 refactor: countID 2024-08-23 17:01:35 -04:00
jstoobysmith
b4c6c3faac refactor: countId (partial) 2024-08-23 15:37:14 -04:00
jstoobysmith
21bbad1e19 refactor: Lint 2024-08-23 11:18:37 -04:00
jstoobysmith
cf0cbb78bb refactor: Index notation 2024-08-23 11:14:48 -04:00
jstoobysmith
097571453f refactor: Lint 2024-08-23 09:49:16 -04:00
jstoobysmith
971291e760 feat: Induction on ColorIndexList 2024-08-23 09:29:39 -04:00
jstoobysmith
5bb9477ec2 refactor: Lint 2024-08-21 10:56:25 -04:00
jstoobysmith
d376632751 feat: Relationship between indices and countP 2024-08-21 10:53:36 -04:00
jstoobysmith
c2eb4bbe9d refactor: Lint 2024-08-21 06:45:09 -04:00
jstoobysmith
c0499483a8 refactor: Last batch of multi-goal proofs 2024-08-21 06:40:58 -04:00
jstoobysmith
b9479c904d refactor: more multiple-goals 2024-08-20 15:27:45 -04:00
jstoobysmith
01f9f7da8b refactor: Split more multi-goal proofs 2024-08-20 15:10:43 -04:00
jstoobysmith
c89a7fd1ea refactor: multiple goal proves 2024-08-20 14:38:29 -04:00
jstoobysmith
b5428ac3e2 Docs: Add TODOs 2024-08-20 09:19:40 -04:00
jstoobysmith
03691af72b refactor: Lint 2024-08-20 09:12:53 -04:00
jstoobysmith
7dff980ae8 feat: List properties of contrIndexList 2024-08-20 09:09:13 -04:00
jstoobysmith
f01ca14f50 refactor: lint 2024-08-19 09:29:45 -04:00
jstoobysmith
b67a7dbb7f feat: tensorindex rel of withDual empty 2024-08-19 09:23:57 -04:00
jstoobysmith
0bd6f316fe feat: More computable form of contracting indices 2024-08-19 06:34:09 -04:00
jstoobysmith
a3988a49d4 refactor: Lint 2024-08-16 16:15:39 -04:00
jstoobysmith
f75661784a Update Contraction.lean 2024-08-16 16:00:50 -04:00
jstoobysmith
8a0f81ae02 refactor: Index notation, computablity 2024-08-16 15:56:18 -04:00
jstoobysmith
7a5acb9734 Doc: Add TODO 2024-08-15 12:50:01 -04:00
jstoobysmith
a44db0c3c0 Docs: Index notation 2024-08-15 12:39:52 -04:00
jstoobysmith
1c9d66ee19 refactor: Lint 2024-08-15 10:53:30 -04:00
jstoobysmith
3693dee740 refactor: Speed and lint 2024-08-15 10:42:11 -04:00
jstoobysmith
0edce53795 refactor: Lint 2024-08-15 10:16:42 -04:00
jstoobysmith
e458300359 refactor: Delete unused files 2024-08-15 07:30:12 -04:00
jstoobysmith
d419a17448 refactor: Working refactor 2024-08-14 16:55:13 -04:00
jstoobysmith
32fd6721f4 refactor: Index notation 2024-08-13 16:36:42 -04:00
jstoobysmith
26ed9a1831 refactor: Index notation 2024-08-12 14:14:45 -04:00
jstoobysmith
33b83d850b refactor: Index notation 2024-08-10 09:16:52 -04:00
jstoobysmith
a8474233ae refactor: Large, incomplete, refactor of index notation 2024-08-08 16:22:52 -04:00
jstoobysmith
85fc57750d refactor: Lint 2024-08-07 08:56:45 -04:00
jstoobysmith
cfd91f85c7 feat: Addition of tensorindex 2024-08-07 08:50:51 -04:00
jstoobysmith
cecec0c843 refactor: Lint 2024-08-06 15:56:29 -04:00
jstoobysmith
d02e94886d feat: Double contraction of indices lemma 2024-08-06 15:43:58 -04:00