support_map_of_injective — Mathlib

English

If f is injective, then support is preserved under map: supp(map_f p) = supp(p).

Русский

Если f инъективно, то отображение коэффициентов сохраняет опору: supp(map_f p) = supp(p).

LaTeX

$$$ supp(map_f p) = supp(p) $ приInjective(f)$$

Lean4

theorem support_map_of_injective (p : MvPolynomial σ R) {f : R →+* S₁} (hf : Injective f) :
    (map f p).support = p.support := by
  apply Finset.Subset.antisymm
  · exact MvPolynomial.support_map_subset _ _
  simp only [Finset.subset_iff, mem_support_iff]
  intro x hx
  contrapose! hx
  rw [coeff_map, ← f.map_zero] at hx
  exact hf hx

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