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

Initializing...

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