mathlib3

1a0f84c7 - feat(linear_algebra/basic): bundle prod and coprod into linear_equivs (#5992)

feat(linear_algebra/basic): bundle prod and coprod into linear_equivs (#5992) In order to do this, this has to reorder some definitions to make the semimodule structure on linear maps available earlier. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>