isScalarTower_right — Mathlib

English

Let S ⊆ T be subalgebras of A over R and X a type with MulAction A X. Then IsScalarTower (Subtype mem S) (Subtype mem T) X holds; i.e., for all s ∈ S, t ∈ T, x ∈ X, (s t) • x = s • (t • x).

Русский

Пусть S ⊆ T — подпалгебры A над R, и X множество с действием через A. Тогда IsScalarTower (Subtype mem S) (Subtype mem T) X выполняется; то есть для любых s ∈ S, t ∈ T и x ∈ X выполняется (s t) • x = s • (t • x).

LaTeX

$$$\forall s \in S,\forall t \in T,\forall x \in X,\ (s t) \cdot x = s \cdot (t \cdot x)$$$

Lean4

scoped instance isScalarTower_right (X) [MulAction A X] :
    letI := (inclusion h).toModule;
    IsScalarTower S T X :=
  letI := (inclusion h).toModule;
  ⟨fun _ ↦ mul_smul _⟩

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