OAI/GroupTheory/SimpleAmenable/Arithmetic/PropagationArithmetic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.endpointLabel_add line 14
2. theorem OAI.SimpleAmenable.endpointLabel_sub line 17
3. theorem OAI.SimpleAmenable.endpointLabel_intCast line 20
4. theorem OAI.SimpleAmenable.endpointLabel_mul line 22
5. theorem OAI.SimpleAmenable.endpointLabel_mul_bound line 30
6. theorem OAI.SimpleAmenable.exists_source_slope line 41
7. theorem OAI.SimpleAmenable.exists_source_slope_explicit line 58
8. theorem OAI.SimpleAmenable.real_list_sum_nonpos line 69
9. theorem OAI.SimpleAmenable.exists_bounded_step_order line 75
10. theorem OAI.SimpleAmenable.exists_step_order_near_segment line 135