OAI/NumberTheory/DirichletL/Descent/GlobalRetainedGatesBudget.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.InverseMomentGlobalRetainedGates.source_cell_exponent_capline 13 - theorem
OAI.SevenEighths.InverseMomentGlobalRetainedGates.source_cell_mass_gateline 27