mapRangeAlgHom_apply — Mathlib

English

For an algebra hom f: A →ₐ[R] B, an element x ∈ MonoidAlgebra A M, and m ∈ M, the value of mapRangeAlgHom f at x on m equals f applied to the coefficient x(m): mapRangeAlgHom M f x m = f (x m).

Русский

Для алгебра-гомоморфизма f: A →ₐ[R] B; для элемента x ∈ MonoidAlgebra A M и элемента m ∈ M: mapRangeAlgHom M f x m = f (x m).

LaTeX

$$$\\mathrm{mapRangeAlgHom}\\ M f \\; x \\; m = f\\big(x(m)\\big).$$$

Lean4

@[to_additive (attr := simp)]
theorem mapRangeAlgHom_apply (f : A →ₐ[R] B) (x : MonoidAlgebra A M) (m : M) : mapRangeAlgHom M f x m = f (x m) :=
  mapRangeRingHom_apply f.toRingHom x m

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