Commit 2023-08-11 10:51 4716e2a2
View on Github →chore(Analysis/InnerProductSpace/PiL2): Make EuclideanSpace.equiv an abbrev (#6503)
This definition already exists elsewhere more generally, but this spelling is admittedly easier to find.
chore(Analysis/InnerProductSpace/PiL2): Make EuclideanSpace.equiv an abbrev (#6503)
This definition already exists elsewhere more generally, but this spelling is admittedly easier to find.