Commit 2025-05-06 11:37 7ad2131e
View on Github →feat: add {Alg,Linear}Equiv.{prodUnique,uniqueProd} (#24168) Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras. Rebased version of #9105.