`BookProof.ChapterA3n.tensorPow_one` {N : ℕ} : tensorPow (N := N) (fun _ => (1 : Matrix (Fin 4) (Fin 4) ℂ)) = 1

Initializing...

`BookProof.ChapterA3n.tensorPow_one` {N : ℕ} : tensorPow (N := N) (fun _ => (1 : Matrix (Fin 4) (Fin 4) ℂ)) = 1 · Prove2Me