aeval_eq_prod_aroots_sub_of_splits

English

If p splits over id_K, then for any v ∈ L, aeval v p equals leadingCoeff times the product over roots of (v − a).

Русский

Если p распадается над id_K, то для любого v ∈ L выполняется aeval v p = leadingCoeff(p) · ∏_{a ∈ roots(p)}(v − a).

LaTeX

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

Lean4

theorem aeval_eq_prod_aroots_sub_of_splits [Algebra K L] {p : K[X]} (hsplit : Splits (algebraMap K L) p) (v : L) :
    aeval v p = algebraMap K L p.leadingCoeff * ((p.aroots L).map fun a ↦ v - a).prod :=
  by
  rw [← eval_map_algebraMap, eq_prod_roots_of_splits hsplit]
  simp [eval_multiset_prod]

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