prod_id — Mathlib

English

The tensor product of the identity with itself is the identity on the tensor product space.

Русский

Тензорное произведение единицы с единицей равно единице на произведении пространств.

LaTeX

$$\left(\operatorname{id} \otimes' \operatorname{id}\right) = \left(\operatorname{id} : \alpha \otimes \beta \Rightarrow \_\right)$$

Lean4

theorem prod_id : ∀ {n} {α β : TypeVec.{u} n}, (id ⊗' id) = (id : α ⊗ β ⟹ _) :=
  by
  intros
  ext i a
  induction i with
  | fz => cases a; rfl
  | fs _ i_ih => apply i_ih

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