roots_map_of_card_eq_natDegree — Mathlib

English

If p is monic and f is a ring hom A →* B with the same domain assumptions, and hroots holds, then p.roots.map f = (p.map f).roots.

Русский

Пусть p монофиксирован и f — кольцевой гомоморфизм, при условии, что выполняются соглашения об областях и hroots, то p.roots.map f = (p.map f).roots.

LaTeX

$$$\forall {A B} [\text{IsDomain } A] [\text{IsDomain } B] {p : Polynomial A} (f : A \to+* B) (hroots : p.roots.card = p.natDegree) (hm : p.Monic),\; p.roots.map f = (p.map f).roots$$$

Lean4

theorem roots_map_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]} (hm : p.Monic) (f : A →+* B)
    (hroots : p.roots.card = p.natDegree) : p.roots.map f = (p.map f).roots :=
  roots_map_of_map_ne_zero_of_card_eq_natDegree f (map_monic_ne_zero hm) hroots

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