splits_of_algHom — Mathlib

English

If a polynomial f splits over the map algebraMap R K, then for any algebra homomorphism e: K →ₐ[R] L, f splits over algebraMap R L.

Русский

Если f распадается над отображением algebraMap R K, то для любого алгебра-гомоморфизма e: K→ₐ[R] L полином распадается над algebraMap R L.

LaTeX

$$$\forall f:Polynomial\ R[X],\ (Splits (algebraMap R K) f) \Rightarrow \forall e:K\to_{{R}} L,\ Splits (algebraMap R L) f$$$

Lean4

theorem splits_of_algHom {f : R[X]} (h : Splits (algebraMap R K) f) (e : K →ₐ[R] L) : Splits (algebraMap R L) f := by
  rw [← e.comp_algebraMap_of_tower R]; exact splits_comp_of_splits _ _ h

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