map_algebraMap_mul — Mathlib

English

Let f: A →_R B be an R-linear map, and a ∈ A, r ∈ R. Then f( algebraMap R A r * a ) = algebraMap R B r * f(a).

Русский

Пусть f: A →_R B — линейное по отношению к R, a ∈ A, r ∈ R. Тогда f( algebraMap R A r · a ) = algebraMap R B r · f(a).

LaTeX

$$$f(\mathrm{algebraMap}_{R,A}(r) \cdot a) = \mathrm{algebraMap}_{R,B}(r) \cdot f(a).$$$

Lean4

/-- An alternate statement of `LinearMap.map_smul` for when `algebraMap` is more convenient to
work with than `•`. -/
theorem map_algebraMap_mul (f : A →ₗ[R] B) (a : A) (r : R) : f (algebraMap R A r * a) = algebraMap R B r * f a := by
  rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]

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