OAI/Combinatorics/Progressions/Lattices/RationalForecastResidueMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.integerLongPolynomial_characteristic_residue_representative line 19
2. theorem OAI.Erdos3.integerLongPolynomial_characteristic_inactive_split line 32
3. theorem OAI.Erdos3.inactiveResidueCoefficient_mass_le line 71
4. theorem OAI.Erdos3.rationalInactiveResidueCoefficient_mass_le line 88
5. theorem OAI.Erdos3.rationalForecast_order_residue_term_count line 104