OAI/NumberTheory/Ostmann/Arithmetic/DiagonalSmallResidueNormBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.transformFactor_le line 13
2. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.localFactor_le line 20
3. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.productTest_le_modulus line 32
4. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.actual_crtTest_bounds line 46
5. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.actual_small_pointwise_bounds line 56