coeff_rename_eq_zero — Mathlib

English

If for all u with u.mapDomain f = d we have φ.coeff u = 0, then (rename f φ).coeff d = 0.

Русский

Если для всех u с u.mapDomain f = d имеем φ.coeff u = 0, то (rename f φ).coeff d = 0.

LaTeX

$$$ \forall u,\ u.\mapDomain f = d \Rightarrow φ.\coeff u = 0 \;\Rightarrow\; (rename f φ).\coeff d = 0 $$$

Lean4

theorem coeff_rename_eq_zero (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ)
    (h : ∀ u : σ →₀ ℕ, u.mapDomain f = d → φ.coeff u = 0) : (rename f φ).coeff d = 0 := by
  classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction

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