mathlib3

d5e2029d - refactor(linear_algebra/basic): extract definitions about pi types to a new file (#6130)

refactor(linear_algebra/basic): extract definitions about pi types to a new file (#6130) This makes it consistent with how the `prod` definitions are in their own file. With each in its own file, it should be easier to unify the APIs between them. This does not do anything other than copy across the definitions.