OAI/Analysis/JiangSu/TensorProducts/RationalStarHomExtension.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalStarExtension.linear line 17
  2. theorem OAI.RationalStarExtension.linear_eq line 20
  3. theorem OAI.RationalStarExtension.linear_one line 28
  4. theorem OAI.RationalStarExtension.linear_mul line 34
  5. theorem OAI.RationalStarExtension.linear_star line 42
  6. theorem OAI.RationalStarExtension.linear_real line 50
  7. theorem OAI.RationalStarExtension.linear_complex line 70
  8. def OAI.RationalStarExtension.extension line 77
  9. theorem OAI.RationalStarExtension.extension_eq line 86