leadingCoeff_map_of_leadingCoeff_ne_zero

English

If leadingCoeff f is nonzero, then leadingCoeff(p.map f) = f(leadingCoeff p).

Русский

Если leadingCoeff p отображается ненулевым, то leadingCoeff(p.map f) = f(leadingCoeff p).

LaTeX

$$$\\operatorname{leadingCoeff}(p.map\\ f) = f\\big(\\operatorname{leadingCoeff}(p)\\big)$$$

Lean4

theorem leadingCoeff_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
    leadingCoeff (p.map f) = f (leadingCoeff p) :=
  by
  unfold leadingCoeff
  rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]

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