OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSourceFlagPruning.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceFlagPruning.prunedSupport_atom_le line 9
2. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceFlagPruning.prunedSupport_nonneg line 13
3. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceFlagPruning.product_mass_prunedSupport line 18
4. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceFlagPruning.double_sum_update_prunedSupport line 24
5. theorem OAI.Ostmann.Arithmetic.HistoryPairSourceFlagPruning.double_sum_eq_of_nonzero line 35