English
The union of roots of all polynomials of bounded degree with coefficients from a finite set is finite after mapping.
Русский
Суммарное объединение корней всех многочленов с ограниченной степенью и коэффициентами в конечном множестве конечное после отображения.
LaTeX
$$$$ \left(\bigcup_{f:\, R[X],\ natDegree(f) \le d,\ \forall i, f.coeff(i) \in U} (f.map(m)).roots\right) \text{ is finite} $$$$
Lean4
/-- The set of roots of all polynomials of bounded degree and having coefficients in a finite set
is finite. -/
theorem bUnion_roots_finite {R S : Type*} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S] (m : R →+* S) (d : ℕ)
{U : Set R} (h : U.Finite) :
(⋃ (f : R[X]) (_ : f.natDegree ≤ d ∧ ∀ i, f.coeff i ∈ U), ((f.map m).roots.toFinset.toSet : Set S)).Finite :=
Set.Finite.biUnion
(by
-- We prove that the set of polynomials under consideration is finite because its
-- image by the injective map `π` is finite
let π : R[X] → Fin (d + 1) → R := fun f i => f.coeff i
refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)
· exact Set.image_subset_iff.2 fun f hf i _ => hf.2 i
· refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_
exact id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩)
fun _ _ => Finset.finite_toSet _
