English
Among many low-degree polynomials, two have identical coefficients up to a certain degree, hence are equal modulo degrees.
Русский
Среди множества полиномов низкого градуса найдутся два с одинаковыми коэффициентами до данного порядка и равные по степеням.
LaTeX
$$∃ i0 ≠ i1, A(i1) = A(i0)$$
Lean4
/-- If the `R`-integral element `a : S` has coordinates `< y` with respect to some basis `b`,
its norm is strictly less than `normBound abv b * y ^ dim S`. -/
theorem norm_lt {T : Type*} [Ring T] [LinearOrder T] [IsStrictOrderedRing T] (a : S) {y : T}
(hy : ∀ k, (abv (bS.repr a k) : T) < y) : (abv (Algebra.norm R a) : T) < normBound abv bS * y ^ Fintype.card ι :=
by
obtain ⟨i⟩ := bS.index_nonempty
have him : (Finset.univ.image fun k => abv (bS.repr a k)).Nonempty :=
⟨_, Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩⟩
set y' : ℤ := Finset.max' _ him with y'_def
have hy' : ∀ k, abv (bS.repr a k) ≤ y' := by
intro k
exact @Finset.le_max' ℤ _ _ _ (Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩)
have : (y' : T) < y :=
by
rw [y'_def, ← Finset.max'_image (show Monotone (_ : ℤ → T) from fun x y h => Int.cast_le.mpr h) _ (him.image _)]
apply (Finset.max'_lt_iff _ (him.image _)).mpr
simp only [Finset.mem_image]
rintro _ ⟨x, ⟨k, -, rfl⟩, rfl⟩
exact hy k
have y'_nonneg : 0 ≤ y' := le_trans (abv.nonneg _) (hy' i)
apply (Int.cast_le.mpr (norm_le abv bS a hy')).trans_lt
simp only [Int.cast_mul, Int.cast_pow]
apply mul_lt_mul' le_rfl
· exact pow_lt_pow_left₀ this (Int.cast_nonneg.mpr y'_nonneg) (@Fintype.card_ne_zero _ _ ⟨i⟩)
· exact pow_nonneg (Int.cast_nonneg.mpr y'_nonneg) _
· exact Int.cast_pos.mpr (normBound_pos abv bS)
