natPrimesInstance

formal source

 184
 185/-! ## Instance: Integer primes -/
 186
 187instance natPrimesInstance : PrimeNormStructure Nat.Primes where
 188  norm := fun p => (p.val : ℝ)
 189  norm_gt_one := fun p => by exact_mod_cast p.prop.one_lt
 190
 191example (p : Nat.Primes) : 0 < primeJcost p := primeJcost_pos p
 192
 193/-! ## Function-field instance (parameterized) -/
 194
 195/-- The function-field prime norm structure: monic irreducible polynomials
 196    in `F[X]` with norm `q^deg P` where `q = Fintype.card F`.  Parameterized
 197    by the field `F` (so it cannot be a global instance). -/
 198def funcFieldNormStructure (F : Type*) [Field F] [Fintype F]
 199    [DecidableEq F] (h2 : 2 ≤ Fintype.card F) :
 200    PrimeNormStructure {P : Polynomial F // P.Monic ∧ Irreducible P} where
 201  norm := fun P => (Fintype.card F : ℝ) ^ P.val.natDegree
 202  norm_gt_one := fun P => by
 203    have hP_irr : Irreducible P.val := P.prop.2
 204    have hP_ne : P.val ≠ 0 := hP_irr.ne_zero
 205    have hP_deg : 0 < P.val.natDegree := by
 206      rw [Nat.pos_iff_ne_zero]
 207      intro h_zero
 208      obtain ⟨c, hc⟩ := Polynomial.natDegree_eq_zero.mp h_zero
 209      have hc_ne : c ≠ 0 := by
 210        intro h_c_zero
 211        apply hP_ne
 212        rw [← hc, h_c_zero]; simp
 213      have hP_unit : IsUnit P.val := by
 214        rw [← hc]
 215        exact Polynomial.isUnit_C.mpr (isUnit_iff_ne_zero.mpr hc_ne)
 216      exact hP_irr.not_isUnit hP_unit
 217    have hq_real : (1 : ℝ) < (Fintype.card F : ℝ) := by exact_mod_cast h2