liftBaseChangeEquiv_symm_apply

Mathlib.RingTheory.TensorProduct.Basic

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

English

The inverse of the base-change equivalence applied to l gives l(1 ⊗ x).

Русский

Обратный оператор к базовому изменению применим к l и дает l(1 ⊗ x).

LaTeX

$$$ (liftBaseChangeEquiv A).symm\, l\, x = l(1 \\otimes x) $$$

Lean4

@[simp]
theorem liftBaseChangeEquiv_symm_apply (l : A ⊗[R] M →ₗ[A] N) (x) : (liftBaseChangeEquiv A).symm l x = l (1 ⊗ₜ x) :=
  rfl

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

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

Разделы

Аффилиация

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