mulLeft_toAddMonoidHom — Mathlib

English

The linear left-action by a is compatible with the additive monoid structure, giving an additive monoid homomorphism when viewed as a map A → A.

Русский

Левое действие умножения на a совместимо с аддитивной структурой, образуя гомоморфизм по аддитивной моноида, когда рассматривается как отображение A → A.

LaTeX

$$$\\text{mulLeft}(R,a)\\ :\\ A \\to A$ is an AddMonoidHom$$

Lean4

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

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