OAI/Algebra/OddKaplansky/ScalarAlgebra.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.MatrixBlock.block line 15
  2. lemma OAI.OddKaplansky.MatrixBlock.block_zero line 17
  3. lemma OAI.OddKaplansky.MatrixBlock.block_add line 18
  4. lemma OAI.OddKaplansky.MatrixBlock.block_sub line 20
  5. lemma OAI.OddKaplansky.MatrixBlock.block_one line 22
  6. lemma OAI.OddKaplansky.MatrixBlock.block_mul line 29
  7. lemma OAI.OddKaplansky.MatrixBlock.block_sandwich line 56
  8. lemma OAI.OddKaplansky.MatrixBlock.block_injective line 71
  9. theorem OAI.OddKaplansky.MatrixBlock.scalar_witnesses line 81
  10. def OAI.OddKaplansky.ProductAlgebras.leftMap line 115
  11. def OAI.OddKaplansky.ProductAlgebras.rightMap line 117
  12. lemma OAI.OddKaplansky.ProductAlgebras.left_right_commute line 120
  13. lemma OAI.OddKaplansky.ProductAlgebras.product_coeff line 133
  14. lemma OAI.OddKaplansky.ProductAlgebras.product_ne_zero line 155
  15. def OAI.OddKaplansky.MatrixBlock.output line 177
  16. lemma OAI.OddKaplansky.MatrixBlock.output_formula line 179
  17. theorem OAI.OddKaplansky.MatrixBlock.prescribed_scalar_products line 187