isScalarTower_finsupp — Mathlib

English

If b is a basis of M over S, then there is a scalar tower structure on ι →₀ S (the Finsupp module) with R to S to ι →₀ S.

Русский

Если b — база M над S, то существует структура скалярной башни на ι →₀ S с R→S→ι →₀ S.

LaTeX

$$$$ IsScalarTower R S (ι \to₀ S) $$$$

Lean4

theorem isScalarTower_finsupp {ι} (b : Basis ι S A) : IsScalarTower R S (ι →₀ S) :=
  b.repr.symm.isScalarTower_of_injective R b.repr.symm.injective

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