piTensorHomMap_tprod_eq_map — Mathlib

English

The map induced by the identity family equals the identity map on the tensor product of the s_i.

Русский

Отображение, индуцированное тождественным отображением, равно тождественному отображению на тензорном произведении.

LaTeX

$$$\mathrm{piTensorHomMap}\_{id} = \mathrm{id}$$$

Lean4

theorem piTensorHomMap_tprod_eq_map (f : Π i, s i →ₗ[R] t i) : piTensorHomMap (tprod R f) = map f := by ext; simp

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