lTensor_id

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

Restricting scalars after applying lTensor is the same as applying lTensor after restricting the scalar.

Русский

После применения lTensor ограничение скаляр эквивалентно применению lTensor после ограничения скаляра.

LaTeX

$$$ (lTensor\; A\; M\ f).restrictScalars R = f.lTensor M$$$

Lean4

@[simp]
theorem lTensor_id : lTensor A M (id : N →ₗ[R] N) = .id :=
  ext fun _ _ => rfl

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

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

Разделы

Аффилиация

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