esymmAlgHomMonomial_single_one — Mathlib

English

Let σ and R be as above. For every i with i ∈ Fin n and every k ∈ ℕ, the value of esymmAlgMonomial on the singleton exponent vector Finsupp.single i k and the scalar 1 equals esymm σ R (i+1) raised to the k-th power. In symbols, esymmAlgMonomial σ (Finsupp.single i k) 1 = esymm σ R (i+1) ^ k.

Русский

Пусть σ и R заданы. Для любого i ∈ Fin n и любого k ∈ ℕ значение esymmAlgMonomial на вектор-степень-единица Finsupp.single i k и скаляре 1 равно esymm σ R (i+1) в степени k, то есть esymmAlgMonomial σ (Finsupp.single i k) 1 = esymm σ R (i+1) ^ k.

LaTeX

$$$\operatorname{esymmAlgMonomial} \sigma (Finsupp.single i k) 1 = \operatorname{esymm} \sigma R (i + 1)^k$$$

Lean4

theorem esymmAlgHomMonomial_single_one : esymmAlgHomMonomial σ (Finsupp.single i k) 1 = esymm σ R (i + 1) ^ k := by
  rw [esymmAlgHomMonomial_single, map_one, one_mul]

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