baseChange_one

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#LinearMap.baseChange_one

English

For any R-module M, baseChange_A(1) equals the identity on A ⊗ M.

Русский

Для любого модуля M над R элемент baseChange_A(1) равен тождественному отображению на A ⊗ M.

LaTeX

$$$$\\mathrm{baseChange}_A(\\mathrm{id})=\\mathrm{id}_{A\\otimes_R M}.$$$$

Lean4

@[simp]
theorem baseChange_one : (1 : Module.End R M).baseChange A = 1 :=
  baseChange_id

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

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

Разделы

Аффилиация

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