Commit 2025-02-21 16:47 5b1b3d74

feat(Logic/Equiv): Upgrade arrowProdEquivProdArrow to dependent types (#21518) This meant the order of arguments had to change a bit, but besides that I think this is strictly more flexible without sacrificing meaningful usability. Also added @[simps]. Upstreamed from quantumInfo