nextCoeff_map — Mathlib

English

For an injective ring hom f and polynomial p, the nextCoeff after map equals the map of nextCoeff: nextCoeff(p.map f) = f(nextCoeff p).

Русский

Для инъективного отображения f и полинома p следующая коэффициента после отображения равна отображению следующего коэффициента: nextCoeff(p.map f) = f(nextCoeff p).

LaTeX

$$$\forall {R} {S} [\text{Semiring } R] [\text{Semiring } S] {f : R \rightarrow+* S} (hf : Injective f) {p : R[X]}, nextCoeff (p.map f) = f (nextCoeff p)$$$

Lean4

theorem nextCoeff_map (hf : Injective f) (p : R[X]) : (p.map f).nextCoeff = f p.nextCoeff :=
  by
  unfold nextCoeff
  rw [natDegree_map_eq_of_injective hf]
  split_ifs <;> simp [*]

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