eval₂Hom_monomial — Mathlib

English

Let f : R →+* S1, g : σ → S1, d : σ →₀ ℕ with finite support, and r ∈ R. Then eval₂Hom f g (monomial d r) = f(r) · ∏ i ∈ supp(d) g(i)^{d(i)}.

Русский

Пусть f : R →+* S1, g : σ → S1, d : σ →₀ ℕ с конечной опорой, и r ∈ R. Тогда eval₂Hom f g(monomial(d,r)) = f(r) · ∏_{i∈supp(d)} g(i)^{d(i)}.

LaTeX

$$$\\mathrm{eval}_2 f g(\\mathrm{monomial}(d,r)) = f(r) \\cdot \\prod_{i \\in \\operatorname{supp}(d)} g(i)^{d(i)}$$$

Lean4

theorem eval₂Hom_monomial (f : R →+* S₁) (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :
    eval₂Hom f g (monomial d r) = f r * d.prod fun i k => g i ^ k := by
  simp only [monomial_eq, RingHom.map_mul, eval₂Hom_C, Finsupp.prod, map_prod, RingHom.map_pow, eval₂Hom_X']

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