cast_symm

Mathlib.LinearAlgebra.TensorPower.Basic

URI: https://scilib.ai/kg/mathlib#TensorPower.cast_symm

English

The cast operation is symmetric with respect to its index-reversing inverse: (cast h).symm = cast h.symm.

Русский

Операция cast симметрична по отношению к обратной операции изменения индексов: (cast h).symm = cast h.symm.

LaTeX

$$$(cast_R M h).symm = cast_R M h.symm$$

Lean4

@[simp]
theorem cast_symm {i j} (h : i = j) : (cast R M h).symm = cast R M h.symm :=
  reindex_symm _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru