instIsScalarTower — Mathlib

English

Suppose G and G' are groups, with SMul actions on β and an IsScalarTower G G' β. Then the type α ↪ β, with its pointwise action, forms an IsScalarTower: for all g ∈ G, g' ∈ G', and f: α ↪ β, g • (g' • f) = (g • g') • f.

Русский

Пусть G и G' — группы, действующие на β, удовлетворяющие условию IsScalarTower G G' β. Тогда множество вложений α ↪ β, с точечным действием, образует IsScalarTower: ∀ g ∈ G, g' ∈ G', f: α ↪ β, g • (g' • f) = (g • g') • f.

LaTeX

$$$ g \cdot (g' \cdot f) = (g \cdot g') \cdot f $$$

Lean4

instance [Group G] [Group G'] [SMul G G'] [MulAction G β] [MulAction G' β] [IsScalarTower G G' β] :
    IsScalarTower G G' (α ↪ β) :=
  ⟨fun x y z => Function.Embedding.ext fun i => smul_assoc x y (z i)⟩

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