mathlib3

fd0cdaee - feat(linear_algebra/pi): pi_option_equiv_prod (#9003)