That's not exactly clear to mathematicians, who tend to complain about the "ascii art operators". I think you'll usually see def byTwo (inputList : List.N

That's not exactly clear to mathematicians, who tend to complain about the "ascii art operators". I think you'll usually see def byTwo (inputList : List.Nat) := inputList.map (. \* 2) rather than using `<$>`. There's also `inputList |>.map (. * 2)`, but I haven't seen it in any mathlib theory code yet, just Lean core or in metaprogramming.