congr_tmul

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

The heterobasic rid coincides with the regular rid under transformation.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem congr_tmul (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : congr f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  rfl

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

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

Разделы

Аффилиация

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