feat(data/sym/basic): add `fill` `filter_ne` and `sigma_ext` (#16316)
feat(data/sym/basic): add `fill` `filter_ne` and `sigma_ext` (#16316)

Add definitions and lemmas to support a proof for the multinomial theorem.

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>



Co-authored-by: Kyle Miller <04892e540c93233cb5dfa2674fa5218f82feced5@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib