Commit 2021-07-03 09:58 915902e6
View on Github →feat(topology/algebra/multilinear): add a linear_equiv version of pi (#8064)
This is a weaker version of continuous_multilinear_map.piₗᵢ
that requires weaker typeclasses.
Unfortunately I don't understand why the typeclass system continues not to cooperate here, but I suspect it's the same class of problem that plagues dfinsupp
.