aeval_id_rename — Mathlib

English

Evaluating after renaming by f with identity evaluation equals evaluating with f directly, i.e., aeval id of rename f equals aeval f after composing.

Русский

Оценка после переименования f эквивалентна прямой оценке через f, т.е. aeval id после rename f равна aeval f.

LaTeX

$$$\text{aeval id} = \text{aeval } f \circ \text{rename } f$$$

Lean4

theorem aeval_id_rename (f : σ → MvPolynomial τ R) (p : MvPolynomial σ R) : aeval id (rename f p) = aeval f p := by
  rw [aeval_rename, Function.id_comp]

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