OAI/NumberTheory/Jacobsthal/Partitions/GeometricInverseGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.GeometricIsolatedBin.geometric_box_isolated_singleton line 17
2. theorem OAI.Erdos970.NumberTheoryLean.GeometricBinOrdering.left_exponent_mono line 49
3. theorem OAI.Erdos970.NumberTheoryLean.GeometricBinOrdering.isolated_before_bounded_edge line 55
4. theorem OAI.Erdos970.NumberTheoryLean.GeometricInverseGeometry.geometric_inverse_geometry line 76