smulTower'_repr

Mathlib.RingTheory.AlgebraTower

URI: https://scilib.ai/kg/mathlib#Module.Basis.smulTower'_repr

← MathLib Explorer

English

The representation of smulTower' is obtained by swapping the roles of indices in smulTower_repr.

Русский

Представление smulTower' получаем путём обмена ролями индексов в smulTower_repr.

LaTeX

$$$$ smulTower'_repr : (b.repr \circ c.repr) = (smulTower) $$$$

Lean4

theorem smulTower'_repr (x ij) : (b.smulTower' c).repr x ij = b.repr (c.repr x ij.1) ij.2 := by
  rw [smulTower', repr_reindex_apply, smulTower_repr]; rfl

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

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

Разделы

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

Аффилиация

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