OAI/NumberTheory/Jacobsthal/Partitions/ActualBoxFourSum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.ParentTailPartition.aboveIndexSet line 16
2. theorem OAI.Erdos970.NumberTheoryLean.ParentTailPartition.residual_partition_multiplicity line 18
3. def OAI.Erdos970.NumberTheoryLean.ParentTailPartition.parentCofactorSelection line 26
4. theorem OAI.Erdos970.NumberTheoryLean.ParentTailPartition.filled_parent_tail line 29
5. theorem OAI.Erdos970.NumberTheoryLean.FourCoordinateBoxSum.four_selection_sum line 68
6. theorem OAI.Erdos970.NumberTheoryLean.FourCoordinateBoxSum.four_coordinate_sum line 105
7. theorem OAI.Erdos970.NumberTheoryLean.ActualBoxFourSum.actual_box_four_coordinate_sum line 136