rid_tmul

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

Heterobasic rid equals regular rid under natural transformation.

Русский

Гетеробазовая rid равна обычной rid при естественном преобразовании.

LaTeX

$$$\mathrm{rid\_eq\_rid} : AlgebraTensorModule.rid R R M = TensorProduct.rid R M$$$

Lean4

@[simp]
theorem rid_tmul (r : R) (m : M) : AlgebraTensorModule.rid R A M (m ⊗ₜ r) = r • m :=
  rfl

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

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

Разделы

Аффилиация

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