OAI/NumberTheory/Ostmann/Arithmetic/DiagonalSmallResidueNormActualProduct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.SmallIndex line 12
2. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.smallPrime line 14
3. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.smallRetained line 18
4. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.smallCoefficients line 22
5. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.smallResidues line 31
6. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.outerUnitMask line 35
7. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.smallPrime_product line 38
8. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.unitFactor_natCast line 44
9. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.actual_productTest_eq line 53
10. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.outerUnitMask_eq_one line 84
11. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.actual_productTest_eq_of_outer_units line 93