esymmAlgHom_zero — Mathlib

English

For the zero exponent vector, esymmAlgMonomial σ (0 : Fin n →₀ ℕ) r equals C r, i.e., the polynomial is the constant function with value r.

Русский

Для нулевого вектора степеней esymmAlgMonomial σ (0 : Fin n →₀ ℕ) r равен C r, то есть получается константный многочлен значением r.

LaTeX

$$$\operatorname{esymmAlgMonomial} \sigma (0 : Fin n \to₀ \mathbb{N}) r = C r$$$

Lean4

theorem esymmAlgHom_zero : esymmAlgHomMonomial σ (0 : Fin n →₀ ℕ) r = C r := by
  rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]

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