OAI/Algebra/OddKaplansky/SectorConstruction.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.Construction.Gā‚ line 16
  2. instance OAI.OddKaplansky.Construction.(instance at line 17) line 17
  3. abbrev OAI.OddKaplansky.Construction.R line 20
  4. def OAI.OddKaplansky.Construction.f line 21
  5. lemma OAI.OddKaplansky.Construction.f_idem line 22
  6. lemma OAI.OddKaplansky.Construction.f_nonzero line 23
  7. lemma OAI.OddKaplansky.Construction.f_commute line 24
  8. def OAI.OddKaplansky.Construction.original line 35
  9. def OAI.OddKaplansky.Construction.attached line 36
  10. def OAI.OddKaplansky.Construction.P line 38
  11. lemma OAI.OddKaplansky.Construction.f_mul_product line 39
  12. lemma OAI.OddKaplansky.Construction.P_idem line 45
  13. lemma OAI.OddKaplansky.Construction.P_sector line 47
  14. lemma OAI.OddKaplansky.Construction.P_ordered line 48
  15. lemma OAI.OddKaplansky.Construction.fit_upper line 50
  16. abbrev OAI.OddKaplansky.Construction.W line 57
  17. abbrev OAI.OddKaplansky.Construction.N line 58
  18. structure OAI.OddKaplansky.Construction.Rectangular line 59
  19. lemma OAI.OddKaplansky.Construction.rectangular_exists line 66
  20. def OAI.OddKaplansky.Construction.prescribedRectangles line 95
  21. def OAI.OddKaplansky.Construction.ix line 126
  22. abbrev OAI.OddKaplansky.Construction.Small line 127
  23. abbrev OAI.OddKaplansky.Construction.Large line 128
  24. def OAI.OddKaplansky.Construction.C line 129
  25. def OAI.OddKaplansky.Construction.D line 131
  26. lemma OAI.OddKaplansky.Construction.DC line 133
  27. lemma OAI.OddKaplansky.Construction.DC_classical line 146
  28. lemma OAI.OddKaplansky.Construction.C_sector line 149
  29. lemma OAI.OddKaplansky.Construction.D_sector line 151
  30. lemma OAI.OddKaplansky.Construction.d_positive line 163
  31. lemma OAI.OddKaplansky.Construction.sizes line 174
  32. lemma OAI.OddKaplansky.Construction.small_positive line 183