leadingCoeff_smul_integralNormalization

English

For any commutative semiring and ring hom, the evaluation at f(p.leadingCoeff)·x of the integralNormalization equals leadingCoeff(p)^{natDegree(p) - 1} times p.eval₂(x).

Русский

Для любой коммутативной полупольной области и гомоморфизма кольца, вычисление eval₂ по f(p.leadingCoeff)·x от integralNormalization равно leadingCoeff(p)^{natDegree(p) - 1} умножить на p.eval₂(x).

LaTeX

$$$\forall f, x:\; (\text{with suitable conditions})\quad (\operatorname{integralNormalization}(p)).\operatorname{eval}_2 f (f(p.leadingCoeff) \cdot x) = f(p.leadingCoeff)^{(p.natDegree - 1)} \cdot p.\operatorname{eval}_2 f x$$$

Lean4

theorem leadingCoeff_smul_integralNormalization (p : S[X]) :
    p.leadingCoeff • integralNormalization p = scaleRoots p p.leadingCoeff := by
  rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]

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