OAI/NumberTheory/Ostmann/Arithmetic/DiagonalSmallResidueNormActualBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.smallProduct line 12
2. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.coefficientDenominator line 14
3. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.small_dvd_smallProduct line 17
4. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.diagonal_denominator_split line 22
5. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.diagonal_modFraction_split line 32
6. def OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.coefficientUnit line 48
7. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.coefficientUnit_coe line 52
8. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.diagonal_factor_eq_transformFactor line 56
9. theorem OAI.Ostmann.Arithmetic.DiagonalSmallResidueNorm.coprime_prod_div_of_pairwise line 69