cardPowDegreeIsAdmissible — Mathlib

English

Given a basis bS of a module S over R, the norm of any integral element a ∈ S is bounded by the product of a norm bound and y^dim(S) when coordinates of a are bounded by y.

Русский

Для базиса bS модуля S над R нормa элемента a ограничена произведением normBound abv bS и y^{dim S}, если координаты a ограничены на y.

LaTeX

$$$\|\!\!$Norm$\!\!$ R a$ \le $normBound abv bS * y^{|ι|}$ при условиях координат <= y.$$

Lean4

/-- `fun p => Fintype.card Fq ^ degree p` is an admissible absolute value.
We set `q ^ degree 0 = 0`. -/
noncomputable def cardPowDegreeIsAdmissible : IsAdmissible (cardPowDegree : AbsoluteValue Fq[X] ℤ) :=
  {
    @cardPowDegree_isEuclidean Fq _
      _ with
    card := fun ε => Fintype.card Fq ^ ⌈-log ε / log (Fintype.card Fq)⌉₊
    exists_partition' := fun n _ hε _ hb => exists_partition_polynomial n hε hb }

Похожие утверждения