`BookProof.SmOneParticle.unitary_row_sum_normSq` (hV : IsMixing V) (i : Fin 3) : ∑ j : Fin 3, ‖V i j‖ ^ 2 = 1

Proved

BookProof.SmOneParticle.unitary_row_sum_normSq

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSmOneParticle.

BookProof.SmOneParticle.unitary_row_sum_normSq (hV : IsMixing V) (i : Fin 3) : ∑ j : Fin 3, ‖V i j‖ ^ 2 = 1

Formalization note: Lean 4 identifier BookProof.SmOneParticle.unitary_row_sum_normSq.

Preamble

-- Generated from ChapterSmOneParticle.lean — theorem BookProof.SmOneParticle.unitary_row_sum_normSq
import Mathlib
import Definitions.Def_ChapterSmOneParticle
open BookProof.SmOneParticle

variable {V U : Matrix (Fin 3) (Fin 3) ℂ}

Formal statement

theorem BookProof.SmOneParticle.unitary_row_sum_normSq (hV : IsMixing V) (i : Fin 3) :
    ∑ j : Fin 3, ‖V i j‖ ^ 2 = 1 := by sorry

View graph