mathlib3

feat(topology/algebra/module): define `fst` and `snd`, review

#2247

Merged