baseChange_id

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

Base-change preserves the identity: baseChange_A(id_M) = id_{A ⊗ M}.

Русский

Расширение сохраняет тождество: baseChange_A(id_M) = id_{A ⊗ M}.

LaTeX

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

Lean4

@[simp]
theorem baseChange_id : (.id : M →ₗ[R] M).baseChange A = .id := by ext; simp

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

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

Разделы

Аффилиация

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