isScalarTower_of_nonempty — Mathlib

English

If there exists a nonempty basis of S over A, then the tower R → S → S satisfies the scalar tower property.

Русский

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

LaTeX

$$$$ isScalarTower R S S $$$$

Lean4

theorem isScalarTower_of_nonempty {ι} [Nonempty ι] (b : Basis ι S A) : IsScalarTower R S S :=
  (b.repr.symm.comp <| lsingle <| Classical.arbitrary ι).isScalarTower_of_injective R
    (b.repr.symm.injective.comp <| single_injective _)

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