kroneckerTMul_smul — Mathlib

English

If a scalar acts on the right factor, the Kron product scales accordingly: A ⊗ (r · B) = r · (A ⊗ B).

Русский

Если скаляр действует на правый фактор, то Kron произведение масштабируется: A ⊗ (r · B) = r · (A ⊗ B).

LaTeX

$$A ⊗ₖₜ[R] (r • B) = r • A ⊗ₖₜ[R] B$$

Lean4

theorem kroneckerTMul_smul [Monoid S] [DistribMulAction S α] [DistribMulAction S β] [SMul S R] [SMulCommClass R S α]
    [IsScalarTower S R α] [IsScalarTower S R β] (r : S) (A : Matrix l m α) (B : Matrix n p β) :
    A ⊗ₖₜ[R] (r • B) = r • A ⊗ₖₜ[R] B :=
  kroneckerMap_smul_right _ _ (fun _ _ => tmul_smul _ _ _) _ _

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