`BookProof.SmGaugeRep.kronecker_sub` (C : Matrix (Fin 3) (Fin 3) ℂ) (A B : Matrix (Fin 2) (Fin 2) ℂ) : C ⊗ₖ (A - B) = C ⊗ₖ A

Initializing...

`BookProof.SmGaugeRep.kronecker_sub` (C : Matrix (Fin 3) (Fin 3) ℂ) (A B : Matrix (Fin 2) (Fin 2) ℂ) : C ⊗ₖ (A - B) = C ⊗ₖ A - C ⊗ₖ B · Prove2Me