smulTower' — Mathlib

English

smulTower' is the reindexed version of smulTower with swapped indices.

Русский

smulTower' — переразиндексированная версия smulTower с поменянными индексами.

LaTeX

$$$$ smulTower' = (b.smulTower c).reindex (Equiv.prodComm ι ι') $$$$

Lean4

/-- `Basis.smulTower (b : Basis ι R S) (c : Basis ι S A)` is the `R`-basis on `A`
where the `(i, j)`th basis vector is `b j • c i`. -/
noncomputable def smulTower' : Basis (ι' × ι) R A :=
  (b.smulTower c).reindex (.prodComm ..)

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