OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkIdentityFrequencyBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.leftData line 11
2. def OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.rightData line 13
3. def OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.leftFactors line 15
4. def OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.rightFactors line 16
5. def OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.leftContext line 17
6. def OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.rightContext line 18
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.exposureStep_left line 20
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.exposureStep_right line 29
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkIdentityFrequency.exposureConstraint_split line 38