tmulEquivDep_symm_apply

Mathlib.LinearAlgebra.PiTensorProduct

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

← MathLib Explorer

English

Compatibility of tmulEquivDep with the currySumEquiv structure.

Русский

Совместимость tmulEquivDep с currySumEquiv.

LaTeX

$$$\\text{tmulEquivDep eq 7}$ expresses compatibility with currySumEquiv.$$

Lean4

@[simp]
theorem tmulEquivDep_symm_apply (f : (i : ι ⊕ ι₂) → N i) :
    (tmulEquivDep R N).symm (⨂ₜ[R] i, f i) = ((⨂ₜ[R] i₁, f (.inl i₁)) ⊗ₜ (⨂ₜ[R] i₂, f (.inr i₂))) := by
  simp [tmulEquivDep]

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

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

Разделы

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

Аффилиация

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