leadingCoeff_of_injective — Mathlib

English

If f is injective, then leadingCoeff(p.map f) = f(leadingCoeff p) for any p ∈ R[X].

Русский

Если f инъективен, то leadingCoeff(p.map f) = f(leadingCoeff p) для любого p ∈ R[X].

LaTeX

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

Lean4

theorem leadingCoeff_of_injective (hf : Injective f) (p : R[X]) : leadingCoeff (p.map f) = f (leadingCoeff p) :=
  by
  delta leadingCoeff
  rw [coeff_map f, natDegree_map_eq_of_injective hf p]

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