R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
⊢ ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
⊢ Multiset.Nodup s
rw [Multiset.nodup_iff_ne_cons_cons]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t)))
⊢ False
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
⊢ ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
rintro a t rfl
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t)))
⊢ (X - ↑C a) * (X - ↑C a) ∣ Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t))
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t)))
⊢ False
refine' not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs _)
no goals
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t)))
⊢ (X - ↑C a) * (X - ↑C a) ∣ Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t))
simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)