English
Basis smulTower combines a basis b for S over R and a basis c for A over S into a basis for A over R, with the (i, j) vector given by b i • c j.
Русский
Basis smulTower объединяет базу b для S над R и базу c для A над S в базу для A над R, где вектор (i, j) равен b i • c j.
LaTeX
$$$$ smulTower : Basis (ι × ι') R A $$$$
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 i • c j`. -/
noncomputable def smulTower : Basis (ι × ι') R A :=
haveI := c.isScalarTower_finsupp R
.ofRepr
(c.repr.restrictScalars R ≪≫ₗ
(Finsupp.lcongr (Equiv.refl _) b.repr ≪≫ₗ
((finsuppProdLEquiv R).symm ≪≫ₗ Finsupp.lcongr (Equiv.prodComm ι' ι) (LinearEquiv.refl _ _))))
