OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSourceLawsSupportBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.PositiveSourceValue line 14
2. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.integerWeight_ne_zero line 17
3. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.positiveSourceValue_of_integerWeight line 31
4. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.PositiveSourceValue.sourceMass line 35
5. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.biasedBlockWeight_source_nonzero line 44
6. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.positiveSourceValue_of_sourceWeight line 55
7. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.positiveSourceValue_of_block_integerWeight line 64