eval₂_X_pow — Mathlib

English

Let f be a ring homomorphism and x an element in the target semiring. Then evaluating the monomial X^n yields x^n for every natural number n.

Русский

Пусть f — кольцевый гомоморфизм и x — элемент целевой полукольца. Тогда при оценке мононима X^n получаем x^n для любого натурального n.

LaTeX

$$$\operatorname{ev}_{f,x}(X^{n}) = x^{n}$$$

Lean4

@[simp]
theorem eval₂_X_pow {n : ℕ} : (X ^ n).eval₂ f x = x ^ n :=
  by
  rw [X_pow_eq_monomial]
  convert eval₂_monomial f x (n := n) (r := 1)
  simp

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