smul_kroneckerTMul — Mathlib

English

If an S-scalar acts on the left, the Kron product scales accordingly: (r · A) ⊗ B = r · (A ⊗ B).

Русский

Если скаляр S действует слева, то равенство сохраняется: (r · A) ⊗ B = r · (A ⊗ B).

LaTeX

$$[Monoid S] [DistribMulAction S α] [SMulCommClass R S α] (r : S) (A : Matrix l m α) (B : Matrix n p β) : (r • A) ⊗ₖₜ[R] B = r • A ⊗ₖₜ[R] B$$

Lean4

theorem smul_kroneckerTMul [Monoid S] [DistribMulAction S α] [SMulCommClass R S α] (r : S) (A : Matrix l m α)
    (B : Matrix n p β) : (r • A) ⊗ₖₜ[R] B = r • A ⊗ₖₜ[R] B :=
  kroneckerMap_smul_left _ _ (fun _ _ => smul_tmul' _ _ _) _ _

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