OAI/NumberTheory/Ostmann/Arithmetic/CompensationEqualityPatternsHistory.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.historyOrigin line 16
2. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.pairedHistoryType line 19
3. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.sum_history_eq_patterns line 23
4. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.sum_pair_history_eq_patterns line 40
5. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.card_pair_history_patterns_le line 66
6. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.pair_history_product_by_multiplicity line 72