Prove2Me

`BookProof.ChapterParityHiggs.pseudoreal_kron_pseudoreal_real` {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m ℂ) (B : Matrix n n ℂ) (hA : A *

Proved
BookProof.ChapterParityHiggs.pseudoreal_kron_pseudoreal_real

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterParityHiggs.

BookProof.ChapterParityHiggs.pseudoreal_kron_pseudoreal_real {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m ℂ) (B : Matrix n n ℂ) (hA : A * A.map (starRingEnd ℂ) = -1) (hB : B * B.map (starRingEnd ℂ) = -1) : (A ⊗ₖ B) * ((A ⊗ₖ B).map (starRingEnd ℂ)) = 1

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

Preamble
-- Generated from ChapterParityHiggs.lean — theorem BookProof.ChapterParityHiggs.pseudoreal_kron_pseudoreal_real
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.pseudoreal_kron_pseudoreal_real
    {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (A : Matrix m m ℂ) (B : Matrix n n ℂ)
    (hA : A * A.map (starRingEnd ℂ) = -1) (hB : B * B.map (starRingEnd ℂ) = -1) :
    (A ⊗ₖ B) * ((A ⊗ₖ B).map (starRingEnd ℂ)) = 1 := by sorry

View graph