support_map_of_injective — Mathlib

English

If f is injective, then the support of map f p equals the support of p.

Русский

Если f инъективно, то поддержка map f p равна поддержке p.

LaTeX

$$$ \\text{Injective}(f) \\Rightarrow (\\mathrm{map}\\ f\\ p).\\mathrm{support} = p.\\mathrm{support} $$$

Lean4

theorem support_map_of_injective [Semiring R] [Semiring S] (p : R[X]) {f : R →+* S} (hf : Function.Injective f) :
    (map f p).support = p.support := by
  simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff, forall_const]

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