OAI/Topology/ArtinGroups/Harmonic/QuantumNumber.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.quantumNumber line 8
2. lemma OAI.HarmonicArtin.quantumNumber_zero line 11
3. lemma OAI.HarmonicArtin.quantum_denominator_pos line 14
4. lemma OAI.HarmonicArtin.quantumNumber_one line 20
5. lemma OAI.HarmonicArtin.quantumNumber_end line 24
6. lemma OAI.HarmonicArtin.quantumNumber_pos line 29
7. lemma OAI.HarmonicArtin.quantumNumber_recurrence line 40
8. abbrev OAI.HarmonicArtin.StringLabel line 51
9. def OAI.HarmonicArtin.stringWeight line 53
10. def OAI.HarmonicArtin.stringMultiplicity line 56
11. lemma OAI.HarmonicArtin.stringWeight_pos line 59
12. lemma OAI.HarmonicArtin.stringMultiplicity_symm line 63
13. lemma OAI.HarmonicArtin.stringMultiplicity_diag line 68
14. lemma OAI.HarmonicArtin.stringMultiplicity_le_one line 71
15. lemma OAI.HarmonicArtin.stringWeight_next line 76
16. lemma OAI.HarmonicArtin.stringWeight_previous line 102
17. lemma OAI.HarmonicArtin.string_dimension_identity line 130