OAI/Combinatorics/Progressions/Results/LinearFormsBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.FixedDensity.AffineForm line 12
2. def OAI.Erdos3.FixedDensity.AffineForm.eval line 18
3. theorem OAI.Erdos3.FixedDensity.AffineForm.eval_zero line 23
4. abbrev OAI.Erdos3.FixedDensity.CubePoint line 30
5. abbrev OAI.Erdos3.FixedDensity.DeletedCube line 33
6. def OAI.Erdos3.FixedDensity.apLinearForm line 36
7. abbrev OAI.Erdos3.FixedDensity.LinearFormsExponent line 41
8. def OAI.Erdos3.FixedDensity.linearFormsProduct line 44
9. def OAI.Erdos3.FixedDensity.HasLinearFormsCondition line 49
10. theorem OAI.Erdos3.FixedDensity.HasLinearFormsCondition.mono line 54