`BookProof.ChapterEulerDensityMatrix.densityMatrix_eq` (t : ℝ) : densityMatrix t = !![Real.cos t ^ 2, Real.cos t * Real.sin t; Real.cos t * Real.sin t, Real.sin t ^ 2]
ProvedBookProof.ChapterEulerDensityMatrix.densityMatrix_eqtheoremstimepiece
Prove the following Lean 4 theorem from ChapterEulerDensityMatrix.
BookProof.ChapterEulerDensityMatrix.densityMatrix_eq (t : ℝ) : densityMatrix t = !![Real.cos t ^ 2, Real.cos t * Real.sin t; Real.cos t * Real.sin t, Real.sin t ^ 2]
Formalization note: Lean 4 identifier BookProof.ChapterEulerDensityMatrix.densityMatrix_eq.
Preamble
-- Generated from ChapterEulerDensityMatrix.lean — theorem BookProof.ChapterEulerDensityMatrix.densityMatrix_eq import Mathlib import Definitions.Def_ChapterEulerDensityMatrix open BookProof.ChapterEulerDensityMatrix open scoped Matrix
Formal statement
theorem BookProof.ChapterEulerDensityMatrix.densityMatrix_eq (t : ℝ) :
densityMatrix t =
!![Real.cos t ^ 2, Real.cos t * Real.sin t;
Real.cos t * Real.sin t, Real.sin t ^ 2] := by sorry