instSMul — Mathlib

English

The action of a group G on a basis is defined by applying the action elementwise to each basis vector, i.e., g • b = b.map (DistribMulAction.toLinearEquiv _ _ g).

Русский

Действие группы G на базисе задаётся покомпонентно: g • b = b.map (DistribMulAction.toLinearEquiv _ _ g).

LaTeX

$$g \cdot b = b.map (\mathrm{DistribMulAction.toLinearEquiv} _ _ g)$$

Lean4

/-- The action on a `Basis` by acting on each element.

See also `Basis.unitsSMul` and `Basis.groupSMul`, for the cases when a different action is applied
to each basis element. -/
instance : SMul G (Basis ι R M) where smul g b := b.map <| DistribMulAction.toLinearEquiv _ _ g

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