mathlib3

aaab1139 - refactor(linear_algebra/prod): split out prod and coprod defs and lemmas (#6059)

refactor(linear_algebra/prod): split out prod and coprod defs and lemmas (#6059) Lemmas are moved without modification. I expect this will take a few builds of adding missing imports.