smul_apply — Mathlib

English

Let R be a commutative ring, A an additive group, and c an element of the character module on A. For any r in R and a in A, the scalar action on c satisfies (r • c)(a) = c(r • a).

Русский

Пусть R — коммутативное кольцо, A — абелева группа, и c ∈ CharacterModule(A). Для любого r ∈ R и a ∈ A выполняется (r • c)(a) = c(r • a).

LaTeX

$$$\forall c \in \mathrm{CharacterModule}(A), \forall r \in R, \forall a \in A, (r \cdot c)(a) = c(r \cdot a)$$$

Lean4

@[simp]
theorem smul_apply (c : CharacterModule A) (r : R) (a : A) : (r • c) a = c (r • a) :=
  rfl

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