OAI/NumberTheory/DirichletL/Moments/DivisorRectangle.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.CenteredMomentDivisorRectangle.factorTupleline 13 - def
OAI.SevenEighths.CenteredMomentDivisorRectangle.selectedPlainline 16 - def
OAI.SevenEighths.CenteredMomentDivisorRectangle.selectedSlotline 19 - theorem
OAI.SevenEighths.CenteredMomentDivisorRectangle.allocationTerm_rectangleline 22 - theorem
OAI.SevenEighths.CenteredMomentDivisorRectangle.double_selected_reindexline 36 - theorem
OAI.SevenEighths.CenteredMomentDivisorRectangle.allocated_rectangle_reindexline 54