OAI/Analysis/Quantum/DimensionTen/NormalizedMatrices.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DimensionTen.Border.NB line 10
2. def OAI.DimensionTen.Border.eQ line 13
3. lemma OAI.DimensionTen.Border.dQ_ne_zero line 15
4. lemma OAI.DimensionTen.Border.cast_mulVec line 17
5. lemma OAI.DimensionTen.Border.cast_single line 22
6. lemma OAI.DimensionTen.Border.normalize_shift line 27
7. lemma OAI.DimensionTen.Border.NB_commute line 38
8. lemma OAI.DimensionTen.Border.QB_annihilator line 59