OAI/Analysis/Quantum/DimensionTen/CompoundTrace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DimensionTen.compound line 13
2. lemma OAI.DimensionTen.exterior_left_entry line 17
3. lemma OAI.DimensionTen.exterior_right_entry line 27
4. lemma OAI.DimensionTen.exterior_compression_entry line 35
5. lemma OAI.DimensionTen.exterior_compound line 48
6. def OAI.DimensionTen.complementaryIndex line 66
7. def OAI.DimensionTen.complementarySign line 67
8. lemma OAI.DimensionTen.hodgeComplement_adjoint line 69
9. lemma OAI.DimensionTen.hodge_mul_entry line 74
10. lemma OAI.DimensionTen.mul_hodge_entry line 80
11. lemma OAI.DimensionTen.compound_trace line 86