OAI/Algebra/OddKaplansky/SquareConstruction.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.Construction.slotOrder line 19
  2. def OAI.OddKaplansky.Construction.lexOrder line 24
  3. def OAI.OddKaplansky.Construction.orderedIndex line 26
  4. def OAI.OddKaplansky.Construction.smallIndex line 28
  5. def OAI.OddKaplansky.Construction.largeIndex line 29
  6. def OAI.OddKaplansky.Construction.inclusion line 31
  7. lemma OAI.OddKaplansky.Construction.inclusion_injective line 32
  8. def OAI.OddKaplansky.Construction.extra line 33
  9. lemma OAI.OddKaplansky.Construction.inclusion_ne_extra line 34
  10. def OAI.OddKaplansky.Construction.squareA line 37
  11. def OAI.OddKaplansky.Construction.squareB line 39
  12. lemma OAI.OddKaplansky.Construction.square_products line 41
  13. lemma OAI.OddKaplansky.Construction.visible_certificate line 48
  14. def OAI.OddKaplansky.Construction.A line 58
  15. def OAI.OddKaplansky.Construction.B line 60
  16. lemma OAI.OddKaplansky.Construction.products line 62
  17. lemma OAI.OddKaplansky.Construction.modulus_ge_two line 74
  18. def OAI.OddKaplansky.Construction.q line 75
  19. abbrev OAI.OddKaplansky.Construction.Λ line 76
  20. abbrev OAI.OddKaplansky.Construction.G line 77
  21. instance OAI.OddKaplansky.Construction.(instance at line 78) line 78
  22. def OAI.OddKaplansky.Construction.a line 80
  23. def OAI.OddKaplansky.Construction.b line 82
  24. lemma OAI.OddKaplansky.Construction.scalar_products line 84
  25. lemma OAI.OddKaplansky.Construction.torsion line 87