mathlib

0be36f6f - feat(data/list/of_fn): Add `list.of_fn_add` and `list.of_fn_mul` (#14370)

feat(data/list/of_fn): Add `list.of_fn_add` and `list.of_fn_mul` (#14370) This adds some lemmas to split up lists generated over `fin (n + m)` and `fin (n * m)` into their constituent parts. It also adds a congr lemma to allow `list.of_fn (λ i : fin n, _)` to be rewritten into `list.of_fn (λ i : fin m, _)` by `simp` when `h : n = m` is available. I'll need these eventually to prove some things about products of tensor powers.