OAI/Analysis/Quantum/DimensionTen/PencilPoints.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DimensionTen.Border.cofactor_last_map line 13
  2. lemma OAI.DimensionTen.Border.rank_embedding line 22
  3. lemma OAI.DimensionTen.Border.root_eq_alpha line 33
  4. lemma OAI.DimensionTen.Border.embedding_points_injective line 37
  5. lemma OAI.DimensionTen.Border.C_relation_map line 54
  6. lemma OAI.DimensionTen.Border.high_relation_point line 63
  7. def OAI.DimensionTen.Border.pointEval line 77
  8. lemma OAI.DimensionTen.Border.pointEval_one line 86
  9. lemma OAI.DimensionTen.Border.pointEval_alpha_mul line 91
  10. lemma OAI.DimensionTen.Border.pointEval_root_mul line 106
  11. lemma OAI.DimensionTen.Border.embedding_of_minor_zero line 113