map_mul_algebraMap — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_mul_algebraMap (f : A →ₗ[R] B) (a : A) (r : R) : f (a * algebraMap R A r) = f a * algebraMap R B r := by
  rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]

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