`BookProof.ChapterBayesInference.joint_sum_one` (hprior_sum : ∑ x, prior x = 1) (hL_row : ∀ x, ∑ y, L x y = 1) : ∑ x, ∑ y, joint prior L x y = 1

Initializing...

`BookProof.ChapterBayesInference.joint_sum_one` (hprior_sum : ∑ x, prior x = 1) (hL_row : ∀ x, ∑ y, L x y = 1) : ∑ x, ∑ y, joint prior L x y = 1 · Prove2Me