tmul_one_eq_one_tmul — Mathlib

English

The tensor product with an algebra map preserves units: algebraMap r ⊗ 1 equals 1 ⊗ algebraMap r.

Русский

Тензорное произведение с отображением алгебры сохраняет единицы: algebraMap r ⊗ 1 = 1 ⊗ algebraMap r.

LaTeX

$$$\mathrm{algebraMap}_R^A(r) \otimes 1 = 1 \otimes \mathrm{algebraMap}_R^B(r)$$$

Lean4

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

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