OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedSpectatorDiagramAverageBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistorySignedSpectatorDiagramAverage.primeAt line 14
2. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectatorDiagramAverage.primeAtNeZero line 16
3. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectatorDiagramAverage.outsideNeZero line 20
4. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectatorDiagramAverage.primeAt_prod line 23
5. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectatorDiagramAverage.primeAt_pairwise line 26
6. def OAI.Ostmann.Arithmetic.HistorySignedSpectatorDiagramAverage.primePair line 35
7. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectatorDiagramAverage.residuePair_eq_projected_product line 40