x ∈ m}` is the product over `m.to_finset` (#8742)

Commit

4 years ago

feat(algebra/big_operators): the product over `{x // x ∈ m}` is the product over `m.to_finset` (#8742)

Author

Vierkantor

Parents