`BookProof.ChapterEulerDensityMatrix.density_euler` (t : ℝ) : densityMatrix t = (1 / 2 : ℝ) • (1 : Matrix (Fin 2) (Fin 2) ℝ) + Zdiag * ((Real.cos (2 * t)) • (1 : Matrix (Fin 2) (Fi

Initializing...

`BookProof.ChapterEulerDensityMatrix.density_euler` (t : ℝ) : densityMatrix t = (1 / 2 : ℝ) • (1 : Matrix (Fin 2) (Fin 2) ℝ) + Zdiag * ((Real.cos (2 * t)) • (1 : Matrix (Fin 2) (Fi · Prove2Me