OAI/Combinatorics/Progressions/Estimates/AllocatedZeroLayerScalarPassage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.IndexedComparableScalarSharedSliceTailStatement line 19
2. theorem OAI.Erdos3.exists_indexed_comparable_scalar_shared_slice_tail line 65
3. theorem OAI.Erdos3.exists_indexed_comparable_scalar_retained_slice_patch line 99
4. theorem OAI.Erdos3.exists_indexed_comparable_scalar_early_retained_slice_patch line 241
5. theorem OAI.Erdos3.exists_indexed_comparable_scalar_physical_family_patch line 340
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedZeroLayer_scalar_passage line 437