English
Let R be a commutative ring with domain, p a prime, and f ∈ R[X]. Then the roots of the expanded polynomial expand R (p^n) f, counted with multiplicities after applying iterateFrobenius R p n, do not exceed p^n times the roots of f; i.e., the multiset of roots under the Frobenius iterate is bounded by p^n times the original root multiset.
Русский
Пусть R — целочисленное кольцо без нулей. Пусть p — простое, f ∈ R[X]. Тогда корни разложения expand R (p^n) f (с учетом кратностей после применения iterateFrobenius R p n) не превосходят p^n кратностей корней f; то есть множество корней после применения Фробениуса ограничено исходным множеством корней.
LaTeX
$$$ (expand R (p^n) f).roots.map (iterateFrobenius R p n) \le p^n \cdot f.roots. $$$
Lean4
theorem roots_expand_pow_map_iterateFrobenius_le :
(expand R (p ^ n) f).roots.map (iterateFrobenius R p n) ≤ p ^ n • f.roots := by
classical
refine le_iff_count.2 fun r ↦ ?_
by_cases h : ∃ s, r = s ^ p ^ n
· obtain ⟨s, rfl⟩ := h
simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map, count_eq_card_filter_eq]
exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
convert Nat.zero_le _
simp_rw [count_map, card_eq_zero]
exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩
