`BookProof.ChapterParityHiggs.kronecker_map_conj` {l m n p : Type*} (A : Matrix l m ℂ) (B : Matrix n p ℂ) : (A ⊗ₖ B).map (starRingEnd ℂ) = (A.map (starRingEnd ℂ)) ⊗ₖ (B.map (starRi

Initializing...

`BookProof.ChapterParityHiggs.kronecker_map_conj` {l m n p : Type*} (A : Matrix l m ℂ) (B : Matrix n p ℂ) : (A ⊗ₖ B).map (starRingEnd ℂ) = (A.map (starRingEnd ℂ)) ⊗ₖ (B.map (starRi · Prove2Me