roots_map_of_map_ne_zero_of_card_eq_natDegree

English

Let A, B be domains and p ∈ A[X], f: A →+* B injective. Then card p.roots ≤ card (p.map f).roots.

Русский

Пусть A, B — области и p ∈ A[X], f: A →+* B инъективен. Тогда card p.roots ≤ card (p.map f).roots.

LaTeX

$$$\forall {A B} [\text{IsDomain } A] [\text{IsDomain } B] {p : Polynomial A} {f : A \to+* B},\; Function.Injective (RingHom.instFunLike.coe f) \Rightarrow \operatorname{card} p.roots \le \operatorname{card} (p.map f).roots$$$

Lean4

theorem roots_map_of_map_ne_zero_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]} (f : A →+* B)
    (h : p.map f ≠ 0) (hroots : p.roots.card = p.natDegree) : p.roots.map f = (p.map f).roots :=
  eq_of_le_of_card_le (map_roots_le h) <| by
    simpa only [Multiset.card_map, hroots] using (p.map f).card_roots'.trans natDegree_map_le

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