LinearEquiv.prodUnique

Stream: mathlib4

[Michael Rothgang]

There are two open PRs defining LinearEquiv.prodUnique: I recently opened #23971 (which will also contain the ContinuousLinearEquiv version), but there is also #9105 (which is delegated, but stale for a year). They use somewhat different approaches - the first PR just takes Equiv.prodUnique and proves the additivity and multiplicativity by simp; the second defines an AddEquiv first and goes via that.

Is there a reason one of these is better than the other? I'd like to understand that better. @Eric Wieser You reviewed #9105 - can you comment which approach seems better to you?

[Eric Wieser]

Defining the addequiv first is better because we should aim to keep the APIs in sync between all the equiv types