pith. machine review for the scientific record. sign in
theorem proved tactic proof

polyPrimeCost_pos

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

formal statement (Lean)

 103theorem polyPrimeCost_pos {P : Polynomial F} (hP : 0 < P.natDegree)
 104    (hF : 2 ≤ Fintype.card F) : 0 < polyPrimeCost P := by

proof body

Tactic-mode proof.

 105  unfold polyPrimeCost
 106  have hnorm_pos : 0 < polyNorm P := polyNorm_pos P
 107  have hnorm_ne_one : polyNorm P ≠ 1 := by
 108    unfold polyNorm
 109    have hq_real : (1 : ℝ) < (Fintype.card F : ℝ) := by
 110      exact_mod_cast hF
 111    have h_pow_gt : 1 < (Fintype.card F : ℝ) ^ P.natDegree :=
 112      one_lt_pow₀ hq_real (Nat.pos_iff_ne_zero.mp hP)
 113    exact ne_of_gt h_pow_gt
 114  exact Jcost_pos_of_ne_one (polyNorm P) hnorm_pos hnorm_ne_one
 115
 116/-- `polyPrimeCost` is nonnegative on any polynomial (it is always `J`
 117    of a positive real). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.