congr_symm_tprod

Mathlib.LinearAlgebra.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.congr_symm_tprod

← MathLib Explorer

English

piTensorHomMap (tprod R f) equals map f.

Русский

piTensorHomMap (tprod R f) равно map f.

LaTeX

$$$\pi\text{TensorHomMap}(\,tprod\ R\ f) = \mathrm{map}\ f$$$

Lean4

@[simp]
theorem congr_symm_tprod (f : Π i, s i ≃ₗ[R] t i) (p : Π i, t i) :
    (congr f).symm (tprod R p) = tprod R (fun (i : ι) ↦ (f i).symm (p i)) := by
  simp only [congr, LinearEquiv.ofLinear_symm_apply, map_tprod, LinearEquiv.coe_coe]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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