rename_isHomogeneous — Mathlib

English

Renaming preserves homogeneity under any injective mapping.

Русский

Переименование сохраняет однородность при любом инъективном отображении.

LaTeX

$$rename_isHomogeneous {f : σ → τ} (h : φ.IsHomogeneous n) : (rename f φ).IsHomogeneous n$$

Lean4

theorem rename_isHomogeneous {f : σ → τ} (h : φ.IsHomogeneous n) : (rename f φ).IsHomogeneous n :=
  by
  rw [← φ.support_sum_monomial_coeff, map_sum]; simp_rw [rename_monomial]
  apply IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _
  intro d hd
  apply (Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans
  convert h (mem_support_iff.mp hd)
  simp only [weight_apply, AddMonoidHom.id_apply, Pi.one_apply, smul_eq_mul, mul_one]

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