toQuadraticMap_smul — Mathlib

English

For any scalar action by S, (a • B).toQuadraticMap = a • B.toQuadraticMap.

Русский

Для скаляльного действия на BilinMap: (a • B).toQuadraticMap = a • B.toQuadraticMap.

LaTeX

$$$ (a \cdot B).toQuadraticMap = a \cdot (B.toQuadraticMap).$$$

Lean4

@[simp]
theorem toQuadraticMap_smul [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] [SMulCommClass R S N] (a : S)
    (B : BilinMap R M N) : (a • B).toQuadraticMap = a • B.toQuadraticMap :=
  rfl

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