baseChange_tmul

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

For a ∈ A and x ∈ M, the base-change of f sends the simple tensor a ⊗ x to the simple tensor a ⊗ f(x): baseChange_A(f)(a ⊗ x) = a ⊗ f(x).

Русский

Для элементов a ∈ A и x ∈ M выполняется baseChange_A(f)(a ⊗ x) = a ⊗ f(x).

LaTeX

$$$$\\mathrm{baseChange}_A(f)(a\\otimes_R x)=a\\otimes_R f(x).$$$$

Lean4

@[simp]
theorem baseChange_tmul (a : A) (x : M) : f.baseChange A (a ⊗ₜ x) = a ⊗ₜ f x :=
  rfl

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

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

Разделы

Аффилиация

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