`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

Proved

BookProof.ChapterParityHiggs.kronecker_map_conj

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterParityHiggs.

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 (starRingEnd ℂ))

Formalization note: Lean 4 identifier BookProof.ChapterParityHiggs.kronecker_map_conj.

Preamble

-- Generated from ChapterParityHiggs.lean — theorem BookProof.ChapterParityHiggs.kronecker_map_conj
import Definitions.Def_ChapterParity
import Mathlib
import Definitions.Def_ChapterParityHiggs
open BookProof.ChapterParityHiggs


open Matrix
open scoped Kronecker
open scoped ComplexConjugate


open BookProof.ChapterParity

Formal statement

theorem 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 (starRingEnd ℂ)) := by sorry

View graph