applyModule — Mathlib

English

The action of CentroidHom α on α is given by evaluation: T • a = T(a).

Русский

Действие CentroidHom α на α задано вычислением: T • a = T(a).

LaTeX

$$$ T \cdot a = T(a) $$$

Lean4

/-- The tautological action by `CentroidHom α` on `α`.

This generalizes `Function.End.applyMulAction`. -/
instance applyModule : Module (CentroidHom α) α where
  smul T a := T a
  add_smul _ _ _ := rfl
  zero_smul _ := rfl
  one_smul _ := rfl
  mul_smul _ _ _ := rfl
  smul_zero := map_zero
  smul_add := map_add

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