OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkIndependentFibreReferenceMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.reference_compatible_all line 23
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.reference_right_mass_nonzero line 27
3. def OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.fixedReferenceTerm line 34
4. def OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.referenceMean line 39
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.term_eq_fixedReferenceTerm line 43
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkIndependentFibreReference.mixedFibreMean_eq_referenceMean line 61