English
Let t and s be finitely supported functions t, s: Fin n → ℕ. Then esymmAlgMonomial σ (t + s) r equals esymmAlgMonomial σ t r times esymmAlgMonomial σ s 1. This expresses a multiplicative compatibility of esymmAlgMonomial with respect to the sum of weight functions.
Русский
Пусть t и s — функции Fin n → ℕ с конечной поддержкой. Тогда esymmAlgMonomial σ (t + s) r равняется произведению esymmAlgMonomial σ t r на esymmAlgMonomial σ s 1. Это выражает совместимость esymmAlgMonomial по отношению к сумме весов.
LaTeX
$$$\operatorname{esymmAlgMonomial} \sigma (t + s) r = \operatorname{esymmAlgMonomial} \sigma t r \; \cdot \; \operatorname{esymmAlgMonomial} \sigma s 1$$$
Lean4
theorem esymmAlgHomMonomial_add {t s : Fin n →₀ ℕ} :
esymmAlgHomMonomial σ (t + s) r = esymmAlgHomMonomial σ t r * esymmAlgHomMonomial σ s 1 := by
simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]
