multiset to function

Stream: new members

[Adam Topaz]

@Mario Carneiro iirc lean4's list.get is a function on fin L.length. Do we have that in mathlib somewhere?

[Adam Topaz]

Of course it's trivial to build using list.nth_le, but still...

[Mario Carneiro]

Are you sure? https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L1103-L1108

[Mario Carneiro]

Mathlib does use this function in a few places (1, 2, 3, 4) but it is always spelled \lam i, l.nth_le i i.2

[Adam Topaz]

@Mario Carneiro , Sorry, I was thinking of Array.get

https://github.com/leanprover/lean4/blob/7ada79bf2ef813424c7a4d5348af379f99395d0a/src/Init/Prelude.lean#L1207