OAI/Algebra/OddKaplansky/SquareCertificate.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.SquareCertificate.cutD line 14
  2. def OAI.OddKaplansky.SquareCertificate.cutC line 15
  3. def OAI.OddKaplansky.SquareCertificate.A line 16
  4. def OAI.OddKaplansky.SquareCertificate.B line 17
  5. lemma OAI.OddKaplansky.SquareCertificate.sector_right line 18
  6. lemma OAI.OddKaplansky.SquareCertificate.complement_left line 19
  7. lemma OAI.OddKaplansky.SquareCertificate.complement_right line 20
  8. lemma OAI.OddKaplansky.SquareCertificate.products line 21
  9. def OAI.OddKaplansky.SquareCertificate.u line 53
  10. def OAI.OddKaplansky.SquareCertificate.v line 54
  11. lemma OAI.OddKaplansky.SquareCertificate.certificate line 55
  12. lemma OAI.OddKaplansky.SquareCertificate.reverse_ne line 93