smulTower_repr_mk

Mathlib.RingTheory.AlgebraTower

URI: https://scilib.ai/kg/mathlib#Module.Basis.smulTower_repr_mk

English

The mk-equivalence of smulTower equals the product mk equivalence.

Русский

Эквивалент mk для smulTower равен произведению mk.

LaTeX

$$$$ smulTower_eq_mk $$$$

Lean4

theorem smulTower_repr_mk (x i j) : (b.smulTower c).repr x (i, j) = b.repr (c.repr x j) i :=
  b.smulTower_repr c x (i, j)

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

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

Разделы

Аффилиация

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