normBound_pos — Mathlib

English

The function p ↦ cardPowDegree(p) defines an admissible absolute value on polynomials over a finite field.

Русский

Функция p ↦ cardPowDegree(p) задаёт допустимую абс. величину на полиномах над конечным полем.

LaTeX

$$IsAdmissible (cardPowDegree : AbsoluteValue Fq[X] ℤ)$$

Lean4

theorem normBound_pos : 0 < normBound abv bS :=
  by
  obtain ⟨i, j, k, hijk⟩ : ∃ i j k, Algebra.leftMulMatrix bS (bS i) j k ≠ 0 :=
    by
    by_contra! h
    obtain ⟨i⟩ := bS.index_nonempty
    apply bS.ne_zero i
    apply (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)
    ext j k
    simp [h]
  simp only [normBound, Algebra.smul_def, eq_natCast]
  apply mul_pos (Int.natCast_pos.mpr (Nat.factorial_pos _))
  refine pow_pos (mul_pos (Int.natCast_pos.mpr (Fintype.card_pos_iff.mpr ⟨i⟩)) ?_) _
  refine lt_of_lt_of_le (abv.pos hijk) (Finset.le_max' _ _ ?_)
  exact Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩

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