functional streams from lean 3

Stream: std4

[Adrien Champion]

A while ago (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/infinite.20lists/near/282588886) I ported the functional streams from Lean 3 to Lean 4. I tried to contribute it to mathlib 4 after the rewrite (which was an exercise) and it ended up not happening.

I was wondering whether it would make sense to have functional streams in std4. I would say "no" as they're more of a mathematical/theoretical notion, but I thought I would ask you guys just in case.