homTensorHomMap_apply

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#TensorProduct.AlgebraTensorModule.homTensorHomMap_apply

English

For r ∈ R and m ∈ M, AlgebraTensorModule.rid R A M sends m ⊗ r to r · m.

Русский

Для r ∈ R и m ∈ M отображение rid отправляет m ⊗ r в r · m.

LaTeX

$$$\mathrm{rid\_tmul}\; (r:\,R)\ (m:\,M) : M ⊗_R R \to_A M\; (m \otimes_R r) = r \cdot m$$$

Lean4

@[simp]
theorem homTensorHomMap_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : homTensorHomMap R A B M N P Q (f ⊗ₜ g) = map f g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru