le_rootMultiplicity_map — Mathlib

English

For a polynomial p ∈ A[x] and a ring hom f : A →+* B with map p ≠ 0, the root multiplicity at a is at most the root multiplicity at f(a) of p map f.

Русский

Для многочлена p ∈ A[x] и кольцевого гомома f: A →+* B, если p maps не равен нулю, тогда кратность корня a не превосходит кратности корня f(a) у p.map f.

LaTeX

$$rootMultiplicity(a, p) ≤ rootMultiplicity(f(a), p.map f)$$

Lean4

theorem le_rootMultiplicity_map {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (a : A) :
    rootMultiplicity a p ≤ rootMultiplicity (f a) (p.map f) :=
  by
  rw [le_rootMultiplicity_iff hmap]
  refine _root_.trans ?_ (_root_.map_dvd (mapRingHom f) (pow_rootMultiplicity_dvd p a))
  rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]

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