splits_iff_mem — Mathlib

English

If p splits over L and F contains all roots, then p splits over F.

Русский

Если p распадается над L и F содержит все корни, то p распадается над F.

LaTeX

$$splits_of_splits$$

Lean4

theorem splits_iff_mem (h : p.Splits (algebraMap K L)) : p.Splits (algebraMap K F) ↔ ∀ x ∈ p.rootSet L, x ∈ F :=
  by
  refine ⟨?_, IntermediateField.splits_of_splits h⟩
  intro hF
  rw [← Polynomial.image_rootSet hF F.val, Set.forall_mem_image]
  exact fun x _ ↦ x.2

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