separable_prod_X_sub_C_iff — Mathlib

English

If (Multiset.map (a ↦ X - C a) s).prod is separable, then s is nodup.

Русский

Если произведение (Multiset.map (a ↦ X − C a) s).prod сепарабельно, то s — без повторов.

LaTeX

$$$ \operatorname{Separable}\left( \operatorname{Multiset.map}(a \mapsto X - C a)\, s \right).prod \Rightarrow s.Nodup$$$

Lean4

theorem separable_prod_X_sub_C_iff {ι : Sort _} [Fintype ι] {f : ι → F} :
    (∏ i, (X - C (f i))).Separable ↔ Function.Injective f :=
  separable_prod_X_sub_C_iff'.trans <| by simp_rw [mem_univ, true_imp_iff, Function.Injective]

Похожие утверждения