`BookProof.ChapterEulerDensityMatrix.densityMatrix_apply_zero` (t : ℝ) : densityMatrix t 0 0 = Real.cos t ^ 2
ProvedBookProof.ChapterEulerDensityMatrix.densityMatrix_apply_zerotheoremstimepiece
Prove the following Lean 4 theorem from ChapterEulerDensityMatrix.
BookProof.ChapterEulerDensityMatrix.densityMatrix_apply_zero (t : ℝ) : densityMatrix t 0 0 = Real.cos t ^ 2
Formalization note: Lean 4 identifier BookProof.ChapterEulerDensityMatrix.densityMatrix_apply_zero.
Preamble
-- Generated from ChapterEulerDensityMatrix.lean — theorem BookProof.ChapterEulerDensityMatrix.densityMatrix_apply_zero import Mathlib import Definitions.Def_ChapterEulerDensityMatrix open BookProof.ChapterEulerDensityMatrix open scoped Matrix
Formal statement
theorem BookProof.ChapterEulerDensityMatrix.densityMatrix_apply_zero (t : ℝ) : densityMatrix t 0 0 = Real.cos t ^ 2 := by sorry