map_one — Mathlib

English

The tensor-product map sends the unit to the unit: applying the tensor-map with the unit in the first component yields the unit in the result.

Русский

Отображение тензорного произведения отправляет единицу в единицу: применение тензорного отображения с единицей в первом компоненте приводит к единице в результате.

LaTeX

$$$ hf.map\; hf\; (1)\; (1) = 1$$$

Lean4

@[simp]
protected theorem map_one : hf.map hf (1 : M₁ →ₗ[R] M₁) (1 : M₂ →ₗ[R] M₂) = 1 :=
  hf.map_id

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