Commit 2021-06-23 23:28 b9ef710e

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).