comapSMul — Mathlib

English

For any g ∈ G, a ∈ α, b ∈ M, the action satisfies g • single a b = single (g • a) b; i.e., the action on a basis element moves the index by g.

Русский

Для любого g ∈ G, a ∈ α, b ∈ M выполнено g • δ_a b = δ_{g•a} b; действие на базисный элемент перемещает индекс по g.

LaTeX

$$@[simp] theorem comapSMul_single (g : G) (a : α) (b : M) : g • single a b = single (g • a) b := mapDomain_single$$

Lean4

/-- Scalar multiplication acting on the domain.

This is not an instance as it would conflict with the action on the range.
See the file `test/instance_diamonds.lean` for examples of such conflicts. -/
def comapSMul [AddCommMonoid M] : SMul G (SkewMonoidAlgebra M α) where smul g := mapDomain (g • ·)

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