Commit 2024-03-20 10:53 9db65796

chore(Data/Funlike): update examples and replace Lean 3 syntax (#11409) Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.