OAI/NumberTheory/Ostmann/Arithmetic/LogCellPartitionIntegerBoundary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.LogCellPartition.integer_log_eq_left_of_closed_not_assigned line 9
2. theorem OAI.Ostmann.Arithmetic.LogCellPartition.integer_closed_assigned_difference_card_le line 21
3. theorem OAI.Ostmann.Arithmetic.LogCellPartition.norm_integer_closed_assigned_test_error line 37
4. def OAI.Ostmann.Arithmetic.LogCellPartition.assignedIntegerResidueMass line 61
5. theorem OAI.Ostmann.Arithmetic.LogCellPartition.integerResidueMass_assigned_error line 66
6. theorem OAI.Ostmann.Arithmetic.LogCellPartition.assignedIntegerResidueMass_error line 87