OAI/Analysis/CoulombIonization/Variational/BlockPermutations.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.blockPermHom line 16
2. def OAI.CoulombAtom.blockPerm line 20
3. def OAI.CoulombAtom.blockSubgroup line 23
4. lemma OAI.CoulombAtom.blockSubgroup_mem line 26
5. lemma OAI.CoulombAtom.blockPerm_apply_left line 30
6. lemma OAI.CoulombAtom.blockPerm_apply_right line 34
7. lemma OAI.CoulombAtom.blockPerm_sign line 38
8. lemma OAI.CoulombAtom.blockSubgroup_mem_of_maps_left line 42
9. lemma OAI.CoulombAtom.leftList_blockPerm line 63
10. lemma OAI.CoulombAtom.rightList_blockPerm line 69