prodMap_id — Mathlib

English

The prodMap of the identity maps is the identity on the product: (id_M) .prodMap (id_M2) = id_{M×M2}.

Русский

Произведение отображений через тождественные отображения дает тождественное отображение на произведении: (id_M) .prodMap (id_M2) = id_{M×M2}.

LaTeX

$$$ (\\mathrm{id} : M \\to M) .prodMap (\\mathrm{id} : M_2 \\to M_2) = \\mathrm{id}_{M \\times M_2}. $$$

Lean4

@[simp]
theorem prodMap_id : (id : M →ₗ[R] M).prodMap (id : M₂ →ₗ[R] M₂) = id :=
  rfl

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