`BookProof.ChapterAttentionMarkov.push_sum_one` {P : Fin m → Fin m → ℝ} {p : Fin m → ℝ} (hP : IsStochastic P) (hp : ∑ j, p j = 1) : ∑ j, push P p j = 1

Initializing...

`BookProof.ChapterAttentionMarkov.push_sum_one` {P : Fin m → Fin m → ℝ} {p : Fin m → ℝ} (hP : IsStochastic P) (hp : ∑ j, p j = 1) : ∑ j, push P p j = 1 · Prove2Me