leadingCoeffHom_apply — Mathlib

English

The action of the leadingCoeffHom on a polynomial p is simply its leading coefficient: leadingCoeffHom(p) = leadingCoeff(p).

Русский

Действие ведущего коэффициента как гомоморфа на многочлене совпадает с самим ведущим коэффициентом: lcHom(p) = lc(p).

LaTeX

$$$\text{leadingCoeffHom}(p)=\text{leadingCoeff}(p).$$$

Lean4

@[simp]
theorem leadingCoeffHom_apply (p : R[X]) : leadingCoeffHom p = leadingCoeff p :=
  rfl

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