English
If f is injective, φ ∈ MvPolynomial σ R and d ∈ σ →₀ ℕ, then (rename f φ).coeff (d.mapDomain f) = φ.coeff d.
Русский
Пусть f инъективно, φ ∈ MvPolynomial σ R и d ∈ σ →₀ ℕ. Тогда (rename f φ).coeff (d.mapDomain f) = φ.coeff d.
LaTeX
$$$ (\mathrm{rename}\ f\ \varphi).\mathrm{coeff}\ (d.\mathrm{mapDomain} f) = \varphi.\mathrm{coeff}\ d $$$
Lean4
@[simp]
theorem coeff_rename_mapDomain (f : σ → τ) (hf : Injective f) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
(rename f φ).coeff (d.mapDomain f) = φ.coeff d := by
classical
apply
φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)
-- Lean could no longer infer the motive
· intro u r
rw [rename_monomial, coeff_monomial, coeff_monomial]
simp only [(Finsupp.mapDomain_injective hf).eq_iff]
· intros
simp only [*, map_add, coeff_add]
