val_mulMap'_tmul

Mathlib.LinearAlgebra.TensorProduct.Submodule

URI: https://scilib.ai/kg/mathlib#Submodule.val_mulMap'_tmul

English

In the opposite-submodule setting, the value on m ∈ M and n ∈ N yields m.1 · n.1 in S.

Русский

В противоположном подмодуле значение на m ∈ M и n ∈ N даёт m.1 · n.1 в S.

LaTeX

$$$(mulMap' M N (m \otimes_R n) : S) = m.1 \cdot n.1$$$

Lean4

@[simp]
theorem val_mulMap'_tmul (m : M) (n : N) : (mulMap' M N (m ⊗ₜ[R] n) : S) = m.1 * n.1 :=
  rfl

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

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

Разделы

Аффилиация

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