chore(data/pi): add pi.prod and use elsewhere (#11877)
`pi.prod` is the function that underlies `add_monoid_hom.prod`, `linear_map.prod`, etc.
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Some.20missing.20prod.20stuff/near/270851797)
