mulRight_toAddMonoidHom — Mathlib

English

For every a ∈ A, the right-multiplication by a, viewed as a map A → A, is the same as the standard AddMonoidHom.mulRight a; i.e., (mulRight R a : A →+ A) = AddMonoidHom.mulRight a.

Русский

Для каждого a ∈ A отображение xb ↦ xb является однородным по сложению и совпадает с обычным гомоморфизмом по аддитивной моноидной структуре: (mulRight R a : A →+ A) = AddMonoidHom.mulRight a.

LaTeX

$$$$ (mulRight\,R\,a : A \to+ A) = AddMonoidHom.mulRight\ a. $$$$

Lean4

@[simp]
theorem mulRight_toAddMonoidHom (a : A) : (mulRight R a : A →+ A) = AddMonoidHom.mulRight a :=
  rfl

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