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