smulTower_repr

Mathlib.RingTheory.AlgebraTower

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

English

The vector corresponding to (i, j) in the smulTower basis equals b i · c j under the representation.

Русский

Вектор, соответствующий паре (i, j) в базе smulTower, равен b i · c j в представлении.

LaTeX

$$$$ (b.smulTower c).repr x = { repr: ... } $$$$

Lean4

@[simp]
theorem smulTower_repr (x ij) : (b.smulTower c).repr x ij = b.repr (c.repr x ij.2) ij.1 := by
  simp [smulTower, Finsupp.uncurry_apply]

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

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

Разделы

Аффилиация

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