rename_isHomogeneous_iff — Mathlib

English

For an injective map f, (rename f φ) is homogeneous of degree n iff φ is homogeneous of degree n.

Русский

Для инъективного отображения f: (rename f φ) однороден степени n тогда и только тогда, когда φ однороден степени n.

LaTeX

$$(rename_isHomogeneous_iff {f : σ → τ} (hf : f.Injective)) : (rename f φ).IsHomogeneous n \leftrightarrow φ.IsHomogeneous n$$

Lean4

theorem rename_isHomogeneous_iff {f : σ → τ} (hf : f.Injective) : (rename f φ).IsHomogeneous n ↔ φ.IsHomogeneous n :=
  by
  refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩
  convert ← @h (d.mapDomain f) _
  · simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]
    exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf
  · rwa [coeff_rename_mapDomain f hf]

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