aeval — Mathlib

English

Renaming variables by an injective mapping preserves the degree of homogeneity.

Русский

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

LaTeX

$$(rename f φ).IsHomogeneous n ←→ φ.IsHomogeneous n, for injective f$$

Lean4

theorem aeval [Algebra R S] (hφ : φ.IsHomogeneous m) (g : σ → MvPolynomial τ S) (hg : ∀ i, (g i).IsHomogeneous n) :
    (aeval g φ).IsHomogeneous (n * m) :=
  hφ.eval₂ _ _ (fun _ ↦ isHomogeneous_C _ _) hg

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