English
If the product (Multiset.map (a ↦ X − C a) s).prod is separable, then the multiset s has no repeated elements.
Русский
Если произведение по множеству Multiset map (a ↦ X − C a) s является сепарабельным, то в multiset s не повторяются элементы.
LaTeX
$$$ \\operatorname{Separable}\\left( \\operatorname{Multiset.map}(a \\mapsto X - C(a))\, s \\right).prod \\Rightarrow s \\text{ is Nodup}$$$
Lean4
theorem nodup_of_separable_prod [Nontrivial R] {s : Multiset R}
(hs : Separable (Multiset.map (fun a => X - C a) s).prod) : s.Nodup :=
by
rw [Multiset.nodup_iff_ne_cons_cons]
rintro a t rfl
refine not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)
simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)
