OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSourceLawsSupportTransport.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.smallSourceSamples_of_roots_occurrencesline 16 - theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.pairedInternalEquiv_originline 43 - theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.pattern_source_occurrence_keyline 51 - theorem
OAI.Ostmann.Arithmetic.HistoryPairSourceLaws.smallSourceSamples_of_pattern_valuesline 65