OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSourceFlagReplacementLaws.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceFlagReplacement.biasedBlockWeight_nonnegline 15 - theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceFlagReplacement.blockNaturalWeight_nonnegline 24 - theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceFlagReplacement.mixedWeight_nonnegline 32 - theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceFlagReplacement.mixedMass_nonnegline 41 - theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceFlagReplacement.dummyMass_nonnegline 52