OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ResidueFiberCard.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.OrdinaryRationalResonance.residue_fiber_cardline 23 - def
OAI.OrdinaryRationalResonance.sameResiduePairsline 44 - lemma
OAI.OrdinaryRationalResonance.pair_count_fibersline 47 - theorem
OAI.OrdinaryRationalResonance.same_residue_pair_countline 58 - lemma
OAI.OrdinaryRationalResonance.off_diagonal_residue_fiberline 66