coeff_rename_embDomain — Mathlib

English

If f is an embedding, then (rename f φ).coeff (d.embDomain f) = φ.coeff d for d in σ →₀ ℕ.

Русский

Если f является вложением, то (rename f φ).coeff (d.embDomain f) = φ.coeff d для d ∈ σ →₀ ℕ.

LaTeX

$$$ (\mathrm{rename}\ f\ \varphi).\mathrm{coeff}\ (d.\embDomain f) = \varphi.\mathrm{coeff}\ d $$$

Lean4

@[simp]
theorem coeff_rename_embDomain (f : σ ↪ τ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
    (rename f φ).coeff (d.embDomain f) = φ.coeff d := by
  rw [Finsupp.embDomain_eq_mapDomain f, coeff_rename_mapDomain f f.injective]

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