OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSpectatorReferenceRawProduct.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.residuePair_eq_projected_product_staticline 18 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.unitTest_eq_raw_of_leavesline 41