subalgebra — Mathlib

English

For any S₀ ⊆ S that is an R-subalgebra, the induced action on A makes R ⟶ S₀ ⟶ A a scalar tower, i.e., IsScalarTower S₀ S A holds.

Русский

Для любого S₀ ⊆ S, являющегося R-подалгеброй, полученное действие на A образует скалярную башню:IsScalarTower S₀ S A.

LaTeX

$$$\text{IsScalarTower } (\text{Subtype }$,mem_S₀\,x) \, S \, A$$$

Lean4

instance subalgebra (S₀ : Subalgebra R S) : IsScalarTower S₀ S A :=
  of_algebraMap_eq fun _ ↦ rfl

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