module module

`IndisputableMonolith.NumberTheory.PrimeCostSpectrumPoly`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (17)

def polyNorm L66
theorem polyNorm_one L69
theorem polyNorm_pos L72
def polyPrimeCost L81
def polyCost L86
theorem polyCost_zero L91
theorem polyCost_one L95
theorem polyPrimeCost_pos L103
theorem polyPrimeCost_nonneg L118
theorem polyCost_nonneg L122
theorem polyCost_mul L134
theorem polyCost_irreducible L145
theorem polyCost_pow L157
theorem polyCost_le_mul L168
lemma irreducible_natDegree_pos L179
theorem polyCost_pos L200
theorem cost_spectrum_poly_certificate L240