OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedResidueFactorizationB.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeSquare_dvd_representativeModulus line 15
  2. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrime_dvd_representativeModulus line 22
  3. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeProjectionB line 26
  4. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeSquareProjectionB line 30
  5. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeLineB line 34
  6. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeSquareLineB line 40
  7. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.finiteOwnPrimeLinesB line 46
  8. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeLineB_intCast line 51
  9. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeSquareLineB_intCast line 58
  10. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.ownPrimeLines_and_squareLines_iff_finiteB line 65