OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSpectatorReferenceRawProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.residuePair_eq_projected_product_static line 18
  2. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.unitTest_eq_raw_of_leaves line 41