mathlib

b9ef710e - chore(linear_algebra): deduplicate `linear_equiv.{Pi_congr_right,pi}` (#8056)

chore(linear_algebra): deduplicate `linear_equiv.{Pi_congr_right,pi}` (#8056) PRs #6415 and #7489 both added the same linear equiv between Pi types. I propose to unify them, using the name of `Pi_congr_right` (more specific, matches `equiv.Pi_congr_right`), the location of `pi` (more specific) and the implementation of `Pi_congr_right` (shorter).