OAI/Analysis/Quantum/DimensionTen/FamilyGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DimensionTen.no_two_zero_cover line 11
2. lemma OAI.DimensionTen.productfree_of_kernel_family line 26
3. lemma OAI.DimensionTen.kronecker_mul_product line 46
4. lemma OAI.DimensionTen.kronecker_product_dot line 59
5. lemma OAI.DimensionTen.psd_summand_kernel line 65
6. lemma OAI.DimensionTen.matrix_nonzero_row line 75
7. lemma OAI.DimensionTen.nonseparable_of_kernel_family line 84