OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkFibreGiantApproximationDefs.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame line 27
  2. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.left line 62
  3. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.right line 64
  4. abbrev OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.Source line 67
  5. abbrev OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.Slots line 69
  6. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.newLeft line 71
  7. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.newRight line 73
  8. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.scalar line 76
  9. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.fixedB line 83
  10. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.residueTest line 88
  11. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.periodic line 95
  12. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.giantIntegral line 101
  13. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.principal line 105
  14. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.sourceMean line 124