applyModule — Mathlib

English

There is a tautological module action of End(A) on A given by evaluation: for e ∈ End(A) and a ∈ A, e • a = e(a).

Русский

Существует тождественное действие End(A) на A, заданное оцениванием: e • a = e(a).

LaTeX

$$$ \text{Module (End(A)) A: } (e,a) \mapsto e(a)$$$

Lean4

/-- The tautological action by `AddMonoid.End α` on `α`.

This generalizes `AddMonoid.End.applyDistribMulAction`. -/
instance applyModule [AddCommMonoid A] : Module (AddMonoid.End A) A
    where
  add_smul _ _ _ := rfl
  zero_smul _ := rfl

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