OAI/Analysis/Quantum/DimensionTen/BorderField.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DimensionTen.Border.fQ line 11
  2. abbrev OAI.DimensionTen.Border.L line 12
  3. instance OAI.DimensionTen.Border.(instance at line 13) line 13
  4. instance OAI.DimensionTen.Border.(instance at line 14) line 14
  5. lemma OAI.DimensionTen.Border.fQ_degree line 16
  6. lemma OAI.DimensionTen.Border.eQ_ne line 20
  7. lemma OAI.DimensionTen.Border.representation_exists line 25
  8. def OAI.DimensionTen.Border.rho line 31
  9. lemma OAI.DimensionTen.Border.rho_root line 33
  10. lemma OAI.DimensionTen.Border.rho_eval_bijective line 36
  11. def OAI.DimensionTen.Border.E line 39
  12. lemma OAI.DimensionTen.Border.E_injective line 44
  13. lemma OAI.DimensionTen.Border.E_surjective line 45
  14. lemma OAI.DimensionTen.Border.E_one line 46
  15. lemma OAI.DimensionTen.Border.E_mul line 47
  16. lemma OAI.DimensionTen.Border.QB_eq line 51
  17. lemma OAI.DimensionTen.Border.NB_in_image line 55
  18. def OAI.DimensionTen.Border.alpha line 61
  19. lemma OAI.DimensionTen.Border.rho_alpha line 64