splits_finsetProd — Mathlib

English

For a finite set s of monics and f ∈ s, f splits in the splitting field of the product ∏ f ∈ s, f.1.

Русский

Для конечного множества s монических многочленов и f ∈ s, f разлагается в разложении произведение над s.

LaTeX

$$$\\forall s:\\mathrm{Finset}(\\mathrm{Monics}(k))\\,\\forall f:\\mathrm{Monics}(k),\\; f \\in s \\Rightarrow \\mathrm{Polynomial}.Splits\\big(\\mathrm{algebraMap}\\ k(\\mathrm{SplittingField}(\\prod f \\in s, f.1))\\big)\\, f.1$$$

Lean4

theorem splits_finsetProd {s : Finset (Monics k)} {f : Monics k} (hf : f ∈ s) :
    f.1.Splits (algebraMap k (SplittingField (∏ f ∈ s, f.1))) :=
  (splits_prod_iff _ fun j _ ↦ j.2.ne_zero).1 (SplittingField.splits _) _ hf

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