aeval_eq_prod_aroots_sub_of_monic_of_splits

English

If p is monic and splits over algebraMap, then aeval v p equals the product over roots with v minus root.

Русский

Если p моноичен и распадается над алгебраMap, то aeval v p равен произведению (v − а) по корням a.

LaTeX

$$$\\forall p:\\ Polynomial K,\\; p.Monic \\Rightarrow \\text{Splits}(\\mathrm{algebraMap}_K L, p) \\Rightarrow \\forall v:\\ L,\\; \\mathrm{aeval}_v(p) = \\big(\\prod_{a \\in p.\\text{aroots }L} (v - a)\\big).$$$

Lean4

theorem aeval_eq_prod_aroots_sub_of_monic_of_splits [Algebra K L] {p : K[X]} (m : Monic p)
    (hsplit : Splits (algebraMap K L) p) (v : L) : aeval v p = ((p.aroots L).map fun a ↦ v - a).prod := by
  simp [aeval_eq_prod_aroots_sub_of_splits hsplit, m]

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