OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkIndependentFibreReferenceSelection.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.Referenceline 20 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.mixedFibreMean_eq_zero_or_referenceline 33