OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSourceLawsMixed.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.SourceIndex line 12
2. def OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixedCarrier line 14
3. instance OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixedCarrierFintype line 21
4. def OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixedValue line 26
5. def OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixedWeight line 33
6. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixedValue_injective line 41
7. def OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixedSupport line 46
8. def OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixedMass line 51
9. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixed_product_sum_reindex line 59
10. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.mixed_weight_product line 72