mulEquiv — Mathlib

English

There is a natural linear isomorphism from ⨂^n M ⊗ ⨂^m M to ⨂^{n+m} M, given by tmulEquiv followed by a canonical reindexing to Fin (n+m).

Русский

Существует естественный линейный изоморфизм ⨂^n M ⊗ ⨂^m M ≅ ⨂^{n+m} M, задаваемый через tmulEquiv и каноническое переназначение индексов Fin (n+m).

LaTeX

$$$\\mathrm{mulEquiv} : ⨂^n M \\otimes_R ⨂^m M \\simeq_L ⨂^{n+m} M$$$

Lean4

/-- A variant of `PiTensorProduct.tmulEquiv` with the result indexed by `Fin (n + m)`. -/
def mulEquiv {n m : ℕ} : ⨂[R]^n M ⊗[R] (⨂[R]^m) M ≃ₗ[R] (⨂[R]^(n + m)) M :=
  (tmulEquiv R M).trans (reindex R (fun _ ↦ M) finSumFinEquiv)

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