eval₂Hom_C — Mathlib

English

Another formulation of eval₂_mul_monomial relating p, monomial, and their evaluations.

Русский

Дополнительная формулировка eval₂_mul_monomial, связывающая p, мономиал и их оценки.

LaTeX

$$$\forall {s,a}, (p \cdot \operatorname{monomial}(s)\; a).eval₂ f g = p.eval₂ f g \cdot f a \cdot s.prod_{n,e} (g n)^e$$$

Lean4

@[simp]
theorem eval₂Hom_C (f : R →+* S₁) (g : σ → S₁) (r : R) : eval₂Hom f g (C r) = f r :=
  eval₂_C f g r

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