OAI/NumberTheory/Ostmann/Arithmetic/HistoryCompensationRepresentativePatternsBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.pairedInternalEquiv line 14
  2. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.pairedInternalEquiv_level line 19
  3. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.natBlockDraw line 25
  4. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeLabel line 39
  5. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeLabel_surjective line 42
  6. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeLabel_eq_iff line 47
  7. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeBlockEquiv line 59
  8. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeBlockEquiv_label line 64
  9. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeBlockEquiv_prime line 69
  10. def OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeFiberEquiv line 75
  11. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representativeBlockEquiv_multiplicity line 87
  12. theorem OAI.Ostmann.Arithmetic.HistoryCompensationRepresentativePatterns.representative_product_eq_blocks line 92