tmulEquiv — Mathlib

English

Equality of two representations of the same dependent tensor product via tmulEquivDep.

Русский

Равенство двух представлений зависимого тензорного произведения через tmulEquivDep.

LaTeX

$$$\\operatorname{tmulEquivDep} = \\text{alternative representation}$$$

Lean4

/-- Equivalence between a `TensorProduct` of `PiTensorProduct`s and a single
`PiTensorProduct` indexed by a `Sum` type.

See `PiTensorProduct.tmulEquivDep` for the dependent version. -/
def tmulEquiv : (⨂[R] (_ : ι), M) ⊗[R] (⨂[R] (_ : ι₂), M) ≃ₗ[R] ⨂[R] (_ : ι ⊕ ι₂), M :=
  tmulEquivDep R (fun _ ↦ M)

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