finiteDimensional_iSup_of_finset'

English

A finite product of polynomials with given splitting fields in subextensions yields a splitting field for the product over the supremum of the subfields. More precisely, if p_i are polynomials with h0 ≠ 0 and each p_i splits in t_i, then the product ∏ p_i splits in ⨆ i∈s, t_i.

Русский

Пусть p_i разбиваются в t_i; тогда произведение p_i разбивается в объединении t_i.

LaTeX

$$$p_i \text{ IsSplittingField}_K(t_i) \;\forall i \in s \quad \Rightarrow\quad (\prod_{i\in s} p_i) \text{ IsSplittingField}_K(\bigsqcup_{i\in s} t_i)$$$

Lean4

theorem finiteDimensional_iSup_of_finset' {s : Finset ι} (h : ∀ i ∈ s, FiniteDimensional K (t i)) :
    FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L) :=
  have := Subtype.forall'.mp h
  iSup_subtype'' s t ▸ IntermediateField.finiteDimensional_iSup_of_finite

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