OAI/Algebra/OddKaplansky/Transfer.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.Heisenberg.matrixEquiv line 15
  2. lemma OAI.OddKaplansky.Heisenberg.matrixEquiv_mul line 18
  3. def OAI.OddKaplansky.Heisenberg.scalar line 21
  4. lemma OAI.OddKaplansky.Heisenberg.scalar_products line 25
  5. lemma OAI.OddKaplansky.Heisenberg.scalar_formula line 39
  6. def OAI.OddKaplansky.Padding.pad line 51
  7. lemma OAI.OddKaplansky.Padding.pad_mul line 52
  8. lemma OAI.OddKaplansky.Padding.pad_one line 53
  9. lemma OAI.OddKaplansky.Padding.pad_ne_one line 60
  10. lemma OAI.OddKaplansky.Padding.products line 72
  11. lemma OAI.OddKaplansky.FixedField.power_search line 84
  12. def OAI.OddKaplansky.FixedField.leastQ line 87
  13. lemma OAI.OddKaplansky.FixedField.leastQ_spec line 88
  14. lemma OAI.OddKaplansky.FixedField.leastQ_min line 89
  15. def OAI.OddKaplansky.FixedField.coordinateOrder line 93
  16. def OAI.OddKaplansky.FixedField.indices line 95
  17. def OAI.OddKaplansky.FixedField.pad line 100
  18. def OAI.OddKaplansky.FixedField.output line 103
  19. lemma OAI.OddKaplansky.FixedField.output_products line 106
  20. lemma OAI.OddKaplansky.FixedField.finite_field_data line 129