esymmAlgHomMonomial_single — Mathlib

English

esymmAlgHomMonomial σ (Finsupp.single i k) r = C(r) · esymm σ R (i+1)^k.

Русский

esymmAlgHomMonomial σ (Finsupp.single i k) r = C(r) · esymm σ R (i+1)^k.

LaTeX

$$$\\mathrm{esymmAlgHomMonomial}_{\\sigma}(σ) (Finsupp.single i k) r = C(r) \\cdot \\mathrm{esymm}_{\\sigma,R}(i+1)^{k}$$$

Lean4

theorem esymmAlgHomMonomial_single : esymmAlgHomMonomial σ (Finsupp.single i k) r = C r * esymm σ R (i + 1) ^ k :=
  by
  rw [esymmAlgHomMonomial, esymmAlgHom_apply, aeval_monomial, algebraMap_eq, Finsupp.prod_single_index]
  exact pow_zero _

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