IndisputableMonolith.NumberTheory.CostTwistedLSeries

declarations in this module (13)

• def twistedPrimeCost L40
• def twistedCostSpectrumValue L45
• theorem twistedCostSpectrumValue_one L48
• theorem twistedCostSpectrumValue_zero L54
• theorem twistedCostSpectrumValue_prime L61
• theorem twistedCostSpectrumValue_pow L69
• theorem twistedCostSpectrumValue_mul L78
• theorem twistedCostSpectrumValue_one_char L93
• theorem twistedCostSpectrumValue_eq_neg L101
• def twistedPrimeCostSum L120
• theorem twistedPrimeCostSum_zero L124
• theorem twistedPrimeCostSum_one_char L131
• theorem cost_twisted_certificate L146