LinearEquiv.uniqueProd [Unique M₁] : M₁ × M₂ ≃ₗ[R] M₂

Stream: Is there code for X?

[Eric Wieser]

We have docs#Equiv.uniqueProd and docs#AddEquiv.uniqueProd, but I can't find docs#LinearEquiv.uniqueProd; do we have it with a weird name?

[Lukas Miaskiwskyi]

Was just looking for exactly the same theorem. Did you end up finding this anywhere? @Eric Wieser

[Eric Wieser]

I think it's missing, PR welcome!

[Eric Wieser]

(for bonus points, add the AlgEquiv versions too)

[Lukas Miaskiwskyi]

PR'd in #9105