OAI/Analysis/GroupDeterminants/LampDenominators.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LampProjectionDraft.fullIntToRat line 15
  2. def OAI.LampProjectionDraft.fullIntToBin line 17
  3. lemma OAI.LampProjectionDraft.fullIntToRat_injective line 20
  4. lemma OAI.LampProjectionDraft.fullIntToRat_baseEmbedding line 23
  5. lemma OAI.LampProjectionDraft.numerator_toRat line 30
  6. lemma OAI.LampProjectionDraft.fullIntToRat_zsmul line 35
  7. lemma OAI.LampProjectionDraft.fullIntToBin_zsmul line 40
  8. lemma OAI.LampProjectionDraft.numerator_square line 45
  9. lemma OAI.LampProjectionDraft.numerator_separates line 52
  10. def OAI.LampProjectionDraft.binaryProjection line 60
  11. lemma OAI.LampProjectionDraft.binaryProjection_idempotent line 63
  12. lemma OAI.LampProjectionDraft.binaryProjection_separates line 69