toAlgHom_monomial — Mathlib

English

The image of a monomial under f.toAlgHom is given by r times the product of f.val(i) raised to the exponent given by v(i).

Русский

Образ монома под f.toAlgHom равен r умножить на произведение f.val(i)^{v(i)}.

LaTeX

$$$f.toAlgHom(\\mathrm{monomial}\\, v\\, r) = r \\cdot \\prod_i f.val(i)^{v(i)}$$$

Lean4

theorem toAlgHom_monomial (f : Generators.Hom P P') (v r) : f.toAlgHom (monomial v r) = r • v.prod (f.val · ^ ·) := by
  rw [toAlgHom, aeval_monomial, Algebra.smul_def]

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