`BookProof.ChapterAttentionMixing.pushIter_succ` (P : Fin m → Fin m → ℝ) (n : ℕ) (p : Fin m → ℝ) : pushIter P (n + 1) p = push P (pushIter P n p)

Initializing...

`BookProof.ChapterAttentionMixing.pushIter_succ` (P : Fin m → Fin m → ℝ) (n : ℕ) (p : Fin m → ℝ) : pushIter P (n + 1) p = push P (pushIter P n p) · Prove2Me