finprod): add finprod.mem_dvd (#9549)

Commit

4 years ago

feat(algebra/big_operators/finprod): add finprod.mem_dvd (#9549) Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Author

mariainesdff

Parents

b2ae1956

mathlib3 845d064a - feat(algebra/big_operators/finprod): add finprod.mem_dvd (#9549)

mathlib3
845d064a - feat(algebra/big_operators/finprod): add finprod.mem_dvd (#9549)