cast — Mathlib

English

There is a canonical linear equivalence cast between ⨂^i M and ⨂^j M when i = j, induced by reindexing along a finite equivalence.

Русский

Существует каноническое линейное эквивалентное отображение cast между ⨂^i M и ⨂^j M при i=j, индуцированное переиндексацией по конечному эквиваленту.

LaTeX

$${i j} (h : i = j) : ⨂^i_M ≃_L ⨂^j_M$$

Lean4

/-- Cast between "equal" tensor powers. -/
def cast {i j} (h : i = j) : ⨂[R]^i M ≃ₗ[R] (⨂[R]^j) M :=
  reindex R (fun _ ↦ M) (finCongr h)

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