def
definition
def or abbrev
funcFieldNormStructure
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Definition body.
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
218 exact one_lt_pow₀ hq_real (Nat.pos_iff_ne_zero.mp hP_deg)
219
220end
221
222end UniversalCostSpectrum
223end NumberTheory
224end IndisputableMonolith