algebraMap_apply — Mathlib

English

There is a variant of the algebra map compatibility: algebraMap S (A ⊗_R B) r = 1_A ⊗_tmul algebraMap S B r.

Русский

Существует вариант совместимости алгебраического отображения: algebraMap S (A ⊗_R B) r = 1_A ⊗_tmul algebraMap S B r.

LaTeX

$$$ algebraMap S (A \otimes_R B) r = 1_A \otimes_\text{tmul} (algebraMap S B r) $$$

Lean4

@[simp]
theorem algebraMap_apply [SMulCommClass R S A] (r : S) : algebraMap S (A ⊗[R] B) r = (algebraMap S A) r ⊗ₜ 1 :=
  rfl

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