English
If the product ∏ i ∈ s (X − C(f_i)) is separable, then the map i ↦ f_i is injective on s.
Русский
Если произведение ∏_{i∈s} (X − C(f_i)) сепарабельно, то отображение i ↦ f_i на s инъективно.
LaTeX
$$$ \operatorname{Separable}\left( \prod_{i\in s} (X - C(f_i)) \right) \Rightarrow \forall x,y \in s, f_x = f_y \Rightarrow x = y$$$
Lean4
theorem inj_of_prod_X_sub_C [Nontrivial R] {ι : Sort _} {f : ι → R} {s : Finset ι}
(hfs : (∏ i ∈ s, (X - C (f i))).Separable) {x y : ι} (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) : x = y := by
classical
by_contra hxy
rw [← insert_erase hx, prod_insert (notMem_erase _ _), ← insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy),
prod_insert (notMem_erase _ _), ← mul_assoc, hfxy, ← sq] at hfs
cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2
