map_id — Mathlib

English

Applying the map to the constant identity maps coordinatewise yields the identity on the tensor product.

Русский

Применение отображения к координатным единицам даёт тождественное отображение на тензорном произведении.

LaTeX

$$$\mathrm{map}(i \mapsto \mathrm{id}_{s_i}) = \mathrm{id}$$$

Lean4

@[simp]
theorem map_id : map (fun i ↦ (LinearMap.id : s i →ₗ[R] s i)) = .id :=
  by
  ext
  simp only [LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.id_coe, id_eq]

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