instSMulCommClass — Mathlib

English

Scaling and reindexing commute: (a • b).reindex e = a • (b.reindex e) for an equivalence e.

Русский

Умножение и переиндексация commute: (a • b).reindex e = a • (b.reindex e).

LaTeX

$$$ (a \\cdot b).reindex e = a \\cdot (b.reindex e)$$$

Lean4

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

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