OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSupportConverseNode.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.node_half_frequency_units_static line 12
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.signed_node_frequency_iff_of_eq_static line 28
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.node_integral_of_frequency_and_own_static line 54