Prove2Me

`BookProof.ChapterParityHiggs.realityOp_realityOp` {I : Type*} [Fintype I] [DecidableEq I] (M : Matrix I I ℂ) (v : I → ℂ) : realityOp M (realityOp M v) = (M * M.map (starRingEnd ℂ)

Proved
BookProof.ChapterParityHiggs.realityOp_realityOp

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterParityHiggs.

BookProof.ChapterParityHiggs.realityOp_realityOp {I : Type*} [Fintype I] [DecidableEq I] (M : Matrix I I ℂ) (v : I → ℂ) : realityOp M (realityOp M v) = (M * M.map (starRingEnd ℂ)) *ᵥ v

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

Preamble
-- Generated from ChapterParityHiggs.lean — theorem BookProof.ChapterParityHiggs.realityOp_realityOp
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.realityOp_realityOp {I : Type*} [Fintype I] [DecidableEq I]
    (M : Matrix I I ℂ) (v : I → ℂ) :
    realityOp M (realityOp M v) = (M * M.map (starRingEnd ℂ)) *ᵥ v := by sorry

View graph