`BookProof.ChapterAttentionMarkov.push_isProb` {P : Fin m → Fin m → ℝ} {p : Fin m → ℝ} (hP : IsStochastic P) (hp : IsProb p) : IsProb (push P p)

Initializing...

`BookProof.ChapterAttentionMarkov.push_isProb` {P : Fin m → Fin m → ℝ} {p : Fin m → ℝ} (hP : IsStochastic P) (hp : IsProb p) : IsProb (push P p) · Prove2Me