natDegree_map_of_leadingCoeff_ne_zero

English

If leadingCoeff p is mapped to a nonzero element, then natDegree(p.map f) = natDegree p.

Русский

Если ведущий коэффициент p отображается в ненулевой элемент, то natDegree(p.map f) = natDegree p.

LaTeX

$$$\\operatorname{natDegree}(p.map\\ f) = \\operatorname{natDegree}(p) \\quad\\text{if } f(leadingCoeff(p)) \\neq 0$$$

Lean4

theorem natDegree_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
    natDegree (p.map f) = natDegree p :=
  natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f hf)

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