algebraMap_apply' — Mathlib

English

A variant of the algebra map formula with different placement of 1’s in the tensors.

Русский

Вариант формулы алгебраического отображения с другой позицией единиц в тензорном произведении.

LaTeX

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

Lean4

theorem algebraMap_apply' (r : R) : algebraMap R (A ⊗[R] B) r = 1 ⊗ₜ algebraMap R B r := by
  rw [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

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