`BookProof.ChapterObservableExpectation.observableExpectation_const` (p : Fin m → ℝ) (hp : ∑ j, p j = 1) (c : E) : observableExpectation p (fun _ => c) = c

Initializing...

`BookProof.ChapterObservableExpectation.observableExpectation_const` (p : Fin m → ℝ) (hp : ∑ j, p j = 1) (c : E) : observableExpectation p (fun _ => c) = c · Prove2Me