English
Two-polynomial closeness lemma for polynomials over a finite field providing an auxiliary bound.
Русский
Лемма о близости двух многочленов в контексте конечного поля с дополнительным ограничением.
LaTeX
$$exists_approx_polynomial_aux _proof_1_1$$
Lean4
/-- If the `R`-integral element `a : S` has coordinates `≤ y` with respect to some basis `b`,
its norm is less than `normBound abv b * y ^ dim S`. -/
theorem norm_le (a : S) {y : ℤ} (hy : ∀ k, abv (bS.repr a k) ≤ y) :
abv (Algebra.norm R a) ≤ normBound abv bS * y ^ Fintype.card ι :=
by
conv_lhs => rw [← bS.sum_repr a]
rw [Algebra.norm_apply, ← LinearMap.det_toMatrix bS]
simp only [map_sum, map_smul, map_sum, map_smul, normBound, smul_mul_assoc, ← mul_pow]
convert Matrix.det_sum_smul_le Finset.univ _ hy using 3
· rw [Finset.card_univ, smul_mul_assoc, mul_comm]
· intro i j k
apply Finset.le_max'
exact Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩
