groupSMul_apply — Mathlib

English

For i, the i-th coordinate of the group-smul basis equals the i-th coordinate of the product of the action and the original basis.

Русский

Для i-й координаты базиса под действием группы равна i-я координата произведения действия и исходного базиса.

LaTeX

$$v.groupSMul w i = (w i) \cdot v i$$

Lean4

theorem groupSMul_apply {G : Type*} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M]
    [SMulCommClass G R M] {v : Basis ι R M} {w : ι → G} (i : ι) : v.groupSMul w i = (w • (v : ι → M)) i :=
  mk_apply (LinearIndependent.group_smul v.linearIndependent w) (groupSMul_span_eq_top v.span_eq).ge i

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