OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedResiduesTest.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.int_modEq_val_pairPrecision line 12
2. def OAI.Ostmann.Arithmetic.HistorySignedResidues.spectatorResidue line 22
3. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.spectatorResidue_intCast line 27
4. def OAI.Ostmann.Arithmetic.HistorySignedResidues.residueTest line 40
5. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.residueTest_intCast line 45
6. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.norm_residueTest_le line 58
7. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.residueTest_intCast_eq_projection line 70