Skip to content

feat(Tensors/Contraction): slot-addressed cross contraction and the general-rank raise/lower round trip - #1375

Merged
jstoobysmith merged 9 commits into
leanprover-community:masterfrom
pariandrea:tensors-bond-contraction
Jul 28, 2026
Merged

feat(Tensors/Contraction): slot-addressed cross contraction and the general-rank raise/lower round trip#1375
jstoobysmith merged 9 commits into
leanprover-community:masterfrom
pariandrea:tensors-bond-contraction

refactor(Tensors): inline the single-consumer index-map lemmas and re…

7d53c31
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Lean based style linters
succeeded Jul 28, 2026 in 7m 40s