OAI/Analysis/CoulombRadii/FieldAnalysis/PermOrCompSwapOffTwo.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.perm_eq_or_comp_swap_of_eq_off_two line 36
2. lemma OAI.Coulomb.perm_mul_swap_ne line 67
3. lemma OAI.Coulomb.permutation_second_minor line 74
4. lemma OAI.Coulomb.sign_star_mul_swap line 97
5. lemma OAI.Coulomb.pair_minor_trace line 103
6. lemma OAI.Coulomb.pair_trace_reindex line 128
7. lemma OAI.Coulomb.slater_two_body_trace_algebra line 145
8. def OAI.Coulomb.pairIndexEquiv line 180
9. def OAI.Coulomb.pairSelectedEquiv line 188
10. def OAI.Coulomb.pairSplit line 193
11. lemma OAI.Coulomb.pairSplit_first line 198
12. lemma OAI.Coulomb.pairSplit_second line 203
13. lemma OAI.Coulomb.pairSplit_rest line 208
14. lemma OAI.Coulomb.pairSplit_measurePreserving line 212
15. lemma OAI.Coulomb.prod_erase_pair line 223
16. lemma OAI.Coulomb.pair_weight_tensor_integrable line 232
17. lemma OAI.Coulomb.pair_weight_tensor_integral line 246