cast_cast

Mathlib.LinearAlgebra.TensorPower.Basic

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

← MathLib Explorer

English

Two successive casts with h and h' are equal to the single cast with h.trans h'.

Русский

Два последовательных cast с h и h' равны одному cast с h.trans h'.

LaTeX

$$cast_R M h' (cast_R M h a) = cast_R M (h.trans h') a$$

Lean4

@[simp]
theorem cast_cast {i j k} (h : i = j) (h' : j = k) (a : ⨂[R]^i M) :
    cast R M h' (cast R M h a) = cast R M (h.trans h') a :=
  reindex_reindex _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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