instIsScalarTower — Mathlib

English

There is a consistent scalar action of two groups G and G' on the vector space V through the affine basis, forming a scalar tower: smul_assoc holds.

Русский

Существует согласованное действие двух групп G и G' на V через аффинную базу, образующее торовую связь: выполняется smul_assoc.

LaTeX

$$$\\text{IsScalarTower}\\ G\\ G'\\ V$ with $smul\\_assoc\\_\\_g\\_\\_g'\\_b$ : $(a\\cdot a')\\; b = a\\; (a'\\; b)$$$

Lean4

/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`. -/
instance [SMul G G'] [IsScalarTower G G' V] : IsScalarTower G G' (AffineBasis ι k V) where
  smul_assoc _g _g' _b := DFunLike.ext _ _ fun _ => smul_assoc _ _ _

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