OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkFibreOriginalReferenceCovariance.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryBulkFibreOriginalReference.bulk_primeMean_relativeline 19 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkFibreOriginalReference.selectedComplexCovariance_eq_fibresline 35 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkFibreOriginalReference.selectedCovariance_eq_fibresline 61