coeFnAddMonoidHom_apply — Mathlib

English

The coercion map from a derivation to its function is an AddMonoidHom; i.e., it preserves addition and zero.

Русский

Соотношение сочетано с преобразованием деривации в её функцию сохраняет сложение и ноль.

LaTeX

$$$\text{coeFnAddMonoidHom} : \mathrm{Derivation}(R,A,M) \to (A \to M)$ is an AddMonoidHom; its action on D is $\text{toFun}(D) = D$.$$

Lean4

@[simp]
theorem coeFnAddMonoidHom_apply (D : Derivation R A M) : coeFnAddMonoidHom D = D :=
  rfl

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