roots_map — Mathlib

English

For f ∈ K[X], if f.Splits i, then the roots of f.map i are exactly the i-images of the roots of f.

Русский

Для f ∈ K[X], если f распадается над i, то корни f.map i равны отображениям корней f через i.

LaTeX

$$$\\forall f:\\ K[X],\\; \\text{Splits }(i,f)\\Rightarrow (f.map i).\\text{roots} = \\mathrm{Multiset}.map i\\ f.\\text{roots}.$$$

Lean4

theorem roots_map {f : K[X]} (hf : f.Splits <| RingHom.id K) : (f.map i).roots = f.roots.map i :=
  (roots_map_of_injective_of_card_eq_natDegree i.injective <|
      by
      convert (natDegree_eq_card_roots hf).symm
      rw [map_id]).symm

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